# Kontrol

## Kontrol

- [Kontrol](https://docs.runtimeverification.com/kontrol/overview/readme.md): Kontrol your smart contracts with formal verification made simple
- [The significance](https://docs.runtimeverification.com/kontrol/overview/readme/the-significance.md): Why Formal Verification with Kontrol?
- [Installations](https://docs.runtimeverification.com/kontrol/overview/readme/installations.md): Everything you need to install
- [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
- [Kup Cheatsheet](https://docs.runtimeverification.com/kontrol/cheatsheets/kup-cheatsheet.md)
- [Kontrol Cheatsheet](https://docs.runtimeverification.com/kontrol/cheatsheets/kontrol-cheatsheet.md): Cheatsheet with (almost) all Kontrol options and gotchas
- [Cheatcodes](https://docs.runtimeverification.com/kontrol/cheatsheets/cheatcodes.md): Learn about Kontrol's cheatcodes for testing and verification
- [Debugging Failing Proofs](https://docs.runtimeverification.com/kontrol/tips/debugging-failing-proofs.md): Tips and tricks for running Kontrol and debugging failing proofs
- [Kontrol Arguments](https://docs.runtimeverification.com/kontrol/glossary/kontrol-arguments.md)
- [Kontrol Build Options](https://docs.runtimeverification.com/kontrol/glossary/kontrol-build-options.md)
- [Kontrol Prove Flags](https://docs.runtimeverification.com/kontrol/glossary/kontrol-prove-flags.md)
- [Digest File](https://docs.runtimeverification.com/kontrol/developer-docs/digest-file.md)
- [Resources](https://docs.runtimeverification.com/kontrol/learn-more/resources.md): Learning materials, community, and educational resources for Kontrol
- [Example Projects](https://docs.runtimeverification.com/kontrol/learn-more/example-projects.md): Code repositories, projects, and practical examples using Kontrol