search

Runtime Verification Docs

kontrol-logoarrow-up-right

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

simbolik-logoarrow-up-right

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-logoarrow-up-right

Kasmer is a tool based on rigorous formal semantics that provides property testing and verification for the MultiversX blockchain.

ERCx-logoarrow-up-right

ERCx a tool built to check the conformance of a contract to the ERC (Ethereum Request for Comments) standardsarrow-up-right.

KaaS-logoarrow-up-right

KaaS CI integrated, cloud-based symbolic execution accessible via an API

[komet]((https://docs.runtimeverification.com/komet/)

hashtag
Join Us

Please come and join us in discordarrow-up-right 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 usarrow-up-right! 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.