| layout |
|---|
landing |
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/)
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.