# 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


---

# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.

## Querying This Documentation
If you need additional information, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on a page URL with the `ask` query parameter:
```
GET https://docs.runtimeverification.com/kontrol/overview/readme.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.