# Runtime Verification Docs

[![kontrol-logo](/files/UbhHFzkxpU1sbz8AeKr6)](https://docs.runtimeverification.com/kontrol/)

[Kontrol](https://docs.runtimeverification.com/kontrol/) combines **KEVM** and Foundry, it grants developers the ability to perform formal verification without learning a new language or tool.

***

[![simbolik-logo](/files/SeVy7F3iVvoDzfFnqkMP)](https://docs.runtimeverification.com/simbolik/)

[Simbolik](https://docs.runtimeverification.com/simbolik/) is a powerful symbolic debugger tailored for debugging Solidity smart contracts. It leverages the capabilities of the **K** framework and employs symbolic execution techniques to meticulously identify potential vulnerabilities in smart contracts.

***

[![kasmer-logo](/files/sxXgIcJ4lKLVJXNkWOa3)](https://docs.runtimeverification.com/kasmer/)

[Kasmer](https://docs.runtimeverification.com/kasmer/) is a tool based on rigorous formal semantics that provides property testing and verification for the MultiversX blockchain.

***

[![ERCx-logo](/files/woeG6zh3xMQ3cFRsP14x)](https://docs.runtimeverification.com/ercx)

[ERCx](https://docs.runtimeverification.com/ercx/) a tool built to check the *conformance* of a contract to the [ERC (Ethereum Request for Comments) standards](https://eips.ethereum.org/erc).

***

[![KaaS-logo](/files/GEla8dS2AgNp98QGqgFU)](https://docs.runtimeverification.com/kaas)

[KaaS](https://docs.runtimeverification.com/kaas) CI integrated, cloud-based symbolic execution accessible via an API

\[komet]\((<https://docs.runtimeverification.com/komet/>)

### Join Us

Please come and join us in [discord](https://discord.com/invite/CurfmXNtbN) and let us know what you would like us to do next. And, if by any chance you are looking for a career change or you are a student looking for an internship, [come and talk to us](https://runtimeverification.com/careers)! We are always looking for exceptional individuals with a passion for formal methods and **K** to join the team in our office in Urbana, Singapore, or remotely from anywhere in the world.


---

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