Welcome to the Runtime Verification blog

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

It's not for some effort towards external transparency, but rather to provide inspiration for those out there that might think "there must be a better way to do business with each other!". If this story of sustainability, transparency, and ultimately decentralization excites you, you might be one of those in the space that maintains a similar ethos to us.

In this blog post, we'd like to share how we build formal verification and fuzzing tools, highlight some of the projects we've developed—such as Kontrol, Kasmer, and Komet — and delve into what it takes to create a tool for formal semantics. Our goal is to provide insights for teams interested in using and developing similar tools for their smart contract languages or ecosystems.

Over the last 6 weeks, Runtime Verification and Term Finance have worked together to formally verify a series of properties that play a key role in the Term Finance’s Tokenized Strategy Protocol.

Our team is already in Thailand, ready to take over DevCon and the side events organized by different teams in the ecosystem! In this blog, we list all the events where our team will be speaking, how to get in touch with us and meet us, and update you on the latest developments in our tooling.

Explore how to leverage Simbolik for streamlined Solidity debugging. Learn to automate deployments, simulate user interactions, and create reusable debugging scenarios—all within Solidity.

This blog post continues our journey into formal verification of loops in Solidity and EVM smart contracts. It introduces loop invariants, a challenging but essential technique for reasoning about unbounded loops. We explore natural induction, apply pen-and-paper methods, and then leverage Kontrol to formally prove the equivalence of two Solidity functions, diving deep into EVM bytecode and formal verification tools.

Explore the challenges of formal verification in Solidity and EVM smart contracts. Learn about the path explosion problem, bounded loop unrolling, and how tools like Certora Prover, Halmos, hevm, and Kontrol approach verifying loops in smart contracts.

we’re excited to introduce our latest tool: Komet, a formal verification and fuzzing tool designed specifically for Soroban smart contracts on the Stellar blockchain.

Komet is supported by the Stellar Foundation and aims to offer enhanced verification capabilities using formal methods to help developers secure their smart contracts.

Stay updated on KMIR's development progress as Runtime Verification defines the semantics of Rust's Middle Intermediate Representation (MIR) in the K Framework. Learn about Stable MIR serialization, the smir_pretty driver, and the future of KMIR's symbolic execution capabilities.