Runtime Verification Docs

Kontrol combines KEVM and Foundry, it grants developers the ability to perform formal verification without learning a new language or tool.

---

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 is a tool based on rigorous formal semantics that provides property testing and verification for the MultiversX blockchain.

---

ERCx a tool built to check the conformance of a contract to the ERC (Ethereum Request for Comments) standards.

---

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 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! 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.