# Resources

Join the Community on [Discord](https://discord.gg/CurfmXNtbN) and [Telegram](https://t.me/rv_kontrol)! If you have questions, feedback, or problems we would love to hear from you and offer support.

## Videos and Presentations

* [Proofcast 105 - Learn Formal Verification in 45 minutes with Kontrol:](https://www.youtube.com/watch?v=iOz8zv_89Bs)
* [Foundry-based Formal Verification with Kontrol](https://www.youtube.com/watch?v=L61GfNMBc14)
* [Verified Hooks: Security, Debugging, and Formal Verification for Uniswap v4](https://www.youtube.com/watch?v=ubOfMnk0HZ0)
* [How To Get Security Under Kontrol](https://www.youtube.com/watch?v=dMoBd0F4cjQ)
* [**K, KEVM, Kontrol** presentation video](https://www.youtube.com/watch?v=9PLnQStkiUo)
* [Tackling Rounding Errors with Precision Analysis](https://youtu.be/nUfcsblYQH0)
* [Formal Methods for the Working DeFi Dev](https://www.youtube.com/watch?v=ETlNhV9jYJw)
* [Security: Auditing and Formal Methods](https://www.youtube.com/watch?v=W_Rs3-Q8pAs)
* [Towards Adoption of Symbolic Execution for DeFi Security](https://www.youtube.com/watch?v=Kjs0ZiZ7m9k)

## Blog Posts and Articles

* [Kontrol and Term Finance: Formal Verification Success Story Working with Bounded Loops](https://www.runtimeverification.com/blog/kontrol-and-term-finance-formal-verification-success-story-working-with-bounded-loops)
* [Formally Verifying Loops: Part 1](https://www.runtimeverification.com/blog/formally-verifying-loops-part-1) and [Part 2](https://www.runtimeverification.com/blog/formally-verifying-loops-part-2)
* [Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs](https://www.runtimeverification.com/blog/using-kontrol-to-tackle-complexities-caused-by-dynamically-sized-constructs)
* [External Computation with Kontrol](https://www.runtimeverification.com/blog/external-computation-with-kontrol)
* [Using Foundry to Explore Upgradeable Contracts (Part 1)](https://runtimeverification.com/blog/using-foundry-to-explore-upgradeable-contracts-part-1)
* [Foundry: Gen 2 of Ethereum Tooling](https://runtimeverification.com/blog/foundry-gen-2-of-ethereum-tooling)
* [From 0 to **K** Tutorial](https://runtimeverification.com/blog/from-0-to-k-tutorial)

## Learning Resources

### Patrick Collins' Course

[Cyfrin's Smart Contract Exploits Course](https://github.com/Cyfrin/sc-exploits-minimized/blob/main/test/invariant-break/formal-verification/KontrolTest.t.sol) includes Kontrol examples as part of their curriculum, showing how to use formal verification to prevent common vulnerabilities.

### Foundry

* [Foundry Book](https://book.getfoundry.sh/) - Comprehensive guide to Foundry
* [Foundry GitHub](https://github.com/foundry-rs/foundry) - Source code and issues

### K Framework

* [K Framework](https://kframework.org/) - The foundation of KEVM and Kontrol
* [0 to K Tutorial](https://runtimeverification.com/blog/from-0-to-k-tutorial) - Learn the K Framework from scratch

### Related Projects

* [KEVM](https://github.com/runtimeverification/evm-semantics) - Ethereum Virtual Machine semantics in K
* [KAVM](https://runtimeverification.com/blog/runtime-verification-brings-formal-verification-to-algorand) - Formal verification for Algorand
* [Komet](https://github.com/runtimeverification/komet) - Testing and formal verification tool for Soroban smart contracts

## Community and Support

* [Discord](https://discord.gg/CurfmXNtbN) and [Telegram](https://t.me/rv_kontrol) community- Join discussions and get help
* [Kontrol GitHub](https://github.com/runtimeverification/kontrol) - Source code, issues, and contributions
* [GitBook Repository](https://github.com/runtimeverification/gitbook-kontrol) - Documentation source and suggestions

{% hint style="info" %}
**Found a typo or want to suggest improvements?** Click the three dots on any page to suggest an edit on [GitHub](https://github.com/runtimeverification/gitbook-kontrol)!
{% endhint %}


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.runtimeverification.com/kontrol/learn-more/resources.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.