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

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.