Runtime Verification Docs


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.



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


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

Last updated