> For the complete documentation index, see [llms.txt](https://docs.runtimeverification.com/kontrol/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.runtimeverification.com/kontrol/learn-more/resources.md).

# 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 %}
