Runtime Verification specializes in formal verification of software systems, providing the highest level of assurance for the correctness and security of smart contracts and other critical software. Our mission is to deliver open-source formal verification and developer tooling to reduce the costs of auditing and enable continuous formal verification and testing on each commit.
Schedule a call with us to discuss formal verification & security engagements, along with custom tooling development & integrations.
Since 2018, we have provided formal verification and security services to numerous blockchain foundations and dApps, such as EigenLayer, Optimism, Uniswap, Ethereum Foundation, Lido, Gnosis, Morpho, Polkadot and many others.
Here you can find a complete list of our previous engagements.
This GitHub Organization hosts all of Runtime Verification's open-source tools and projects, designed to improve the security and reliability of blockchain and software systems through formal verification.
We are currently building and maintaining the following projects:
- K Framework: A rewrite-based executable semantic framework that allows formal definition of programming languages and VMs.
- Kontrol: Combines KEVM and Foundry to enable developers to perform formal verification without learning new languages or tools.
- Simbolik: VSCode-compatible Solidity debugger with built-in symbolic execution engine designed to assist in debugging and verifying smart contracts.
- KEVM: An executable formal specification of the Ethereum Virtual Machine (EVM) in the K framework.
- KWasm: A formal semantics of WebAssembly in the K framework, allowing formal analysis and verification of WebAssembly programs.
- KMIR: A formal semantics of the Rust MIR (Mid-level Intermediate Representation) in the K framework.
- Kasmer: A formal verification tool for WebAssembly, based on KWasm.
- KaaS: CI Integrated Cloud-Based Symbolic Execution.
You can learn more about our tools from Runtime Verification docs.
We invite developers, researchers, and enthusiasts to explore and contribute to our projects, as we continue to push the boundaries of formal verification and secure software development.