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