> 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/guides.md).

# Guides

- [Proofcast Episode: Getting Started](https://docs.runtimeverification.com/kontrol/guides/proofcast-episode.md): Learn Kontrol through a hands-on video tutorial
- [Kontrol Example](https://docs.runtimeverification.com/kontrol/guides/kontrol-example.md): How to run property tests with Kontrol
- [Property Verification using Kontrol](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/property-verification-using-kontrol.md)
- [K Control Flow Graph (KCFG)](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/k-control-flow-graph-kcfg.md): Investigating a failed test and understanding the KCFG output
- [Proof Management](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/proof-management.md)
- [Debugging a Proof](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/linked-library-example.md)
- [Handling Dynamically Sized Inputs](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/dynamic-types.md): How to work with dynamically sized types in Kontrol using NatSpec annotations
- [Compositional Symbolic Execution (CSE) and Node Merging](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/compositional-symbolic-execution.md): Learn about Compositional Symbolic Execution (CSE) and optimization techniques in Kontrol
- [Node Refutation](https://docs.runtimeverification.com/kontrol/guides/node-refutation.md)
- [Bytecode Verification](https://docs.runtimeverification.com/kontrol/guides/bytecode-verification.md)
- [Advancing Proofs](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs.md): How to identify and write lemmas to advance on your proofs
- [KEVM Lemmas](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas.md): How to debug your KCFG and find KEVM reasoning gaps
- [Writing Simplifications](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/simplifications-guide.md): A comprehensive guide to writing simplifications for Kontrol
- [Rule Application](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/rule-application.md): A detailed look at rules and rule application in K
- [Symbolic Storage](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/symbolic-storage.md): Using structured symbolic storage in Kontrol tests
- [Structured Symbolic Storage Generation](https://docs.runtimeverification.com/kontrol/guides/structured-symbolic-storage-generation.md): Automated generation of structured symbolic storage
- [Counterexample Generation](https://docs.runtimeverification.com/kontrol/guides/counterexample-generation.md): Generating counterexamples for failing proofs in Kontrol