# 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


---

# 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/guides.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.