Gregory Makodzeba

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.


blog11.png

Runtime Verification

How We Build Formal Verification and Fuzzing Tools: <br> Bridging the Gap Between Developers and Advanced Security Tooling with the K Framework

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.

Term.png

Term Labs

Kontrol and Term Finance: Formal Verification Success Story Working with Bounded Loops

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.


BDE9AEC9-9415-459A-B4CC-615A34C7C39C.png

Meet the RV Team at DevCon

Raoul Schaffranek

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

simbolik-screenshot.png

 Using Simbolik for Solidity Debugging

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.

DALL·E 2024-09-25 17.50.48 - A futuristic rollercoaster with multiple loopings, representing symbolic execution and bounded loop unrolling. The rollercoaster track is set against .webp

Formally Verifying Loops: Part 2

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.

Formally Verifying Loops: Part 1

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.

256A0EF8-BED9-408A-899E-1839CB2B243E.png

Introducing Komet: Smart Contract Testing & Verification Tool for Soroban, Created by Runtime Verification

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

E6B83973-A395-4089-BDB0-34CEA8DCDDF3.png

How to get started with Komet - Property Testing and Formal Verification for Soroban

Daniel Cumming

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.

DALL·E 2024-09-13 03.23.10 - A flowchart-style diagram depicting the smir_pretty driver pipeline, showing connections between the Rust compiler and Stable MIR without any words or.webp

KMIR: Progress Update

Runtime Verification completed a design review of Lido's dual governance mechanism. This mechanism is the first of its kind, representing a monumental upgrade to the Lido governance model. This collaboration aimed to ensure that the new system, scheduled for testnet release in Q3 2024 and mainnet in Q4 2024, functions as intended and maintains the integrity and security of Lido’s $33 billion in total value locked (as of this writing). 


lido.png

With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review

Juan Conejero

This is the 3rd post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This post will explain a crucial feature we developed in Kontrol to verify the pausability mechanism in a realistic scenario. This new Kontrol feature allows loading a transcript of the effects of executing a function directly into proofs, which effectively means having a part of a Kontrol proof computed by Foundry!


opt3 twitter.png

optimism

External Computation with Kontrol: <br/> Leveraging Foundry Execution for Formal Verification

This is the second post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This installment explains how Kontrol can be used to tackle the complexities caused by dynamically-sized constructs and the challenges associated with the loops that result from them.

opt2 twitter.png

Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs

Learn how Runtime Verification's contribution to the Stable MIR project enhances Rust development by implementing Serde serialization. Discover how this key addition improves accessibility, portability, and future project development using Rust’s Middle Intermediate Representation (MIR).

DALL·E 2024-09-12 06.27.28 - An abstract depiction of Stable MIR, visualizing a stable platform bridging two shifting environments. On one side, a dynamic, changing environment sy.webp

Enhancing Stable MIR with Serde Serialisation

We are pleased to announce our recently completed work with Optimism and Kontrol integration into their CI. Having Kontrol as part of Optimism’s CI produces proof of correctness for critical properties of the code as it evolves.

Opt.kontrol.png

Kontrol Integrated Verification of the Optimism Pausability Mechanism

April 2024 saw the release of version 7.0 of the K Framework. Previously, K was focused on the implementation of programming language semantics, and external tool support was required to expand those semantics into production tooling for a language. In K 7.0, we have merged our Python support library for K (Pyk) into the K compiler, making it the primary way for tool developers to interact with K.


k7.png

K 7.0: Improving K for Ecosystem Tool Developers

On April 14th, Andrej Vacaru and Raoul Schaffranek from Runtime Verification were privileged to lead an online workshop hosted by the EthCluj community. We are sincerely grateful for this opportunity, which allowed us to share our passion for innovative software verification tools with an engaged audience.


ethcluj.png

Runtime Verification Hosts EthCluj Workshop on Formal Methods

This article aims to provide context to formal verification, its different approaches, and why it can provide ultimate assurance of code correctness. Throughout the article, we provide insights into the field of formal verification and some of its components rather than explain how to use a specific tool. These insights should make it clearer to the newcomer to the field why we can claim mathematical rigorousness when we perform formal verification.

fv lore.png

Formal Verification Lore <br> Intuitive Intro to Why We Can Prove Programs Correct <br>

Runtime Verification is pleased to announce the audit completion of Band Protocol’s rust implementation of the Band Standard Reference Soroban Smart Contract. Band Protocol, built on top of Cosmos, is a cross-chain data oracle platform that aggregates and connects real-world data and APIs to smart contracts.


band protocol.png

Band Protocol

Runtime Verification Audits Band Protocol’s Rust Implementation of the Band StandardReference Soroban Smart Contract

Yale Vinson

Palina Tolmach

Recently you may have heard about our new tool Kontrol, but are still uncertain about what it is or how it might benefit your project’s security. This blog post addresses those concerns by explaining the blockchain security lifecycle, how it differs from traditional software security, and the role that Kontrol plays in ensuring that your application is as secure as possible.

kontrol 101.png

Kontrol 101

Runtime Verification is pleased to announce Synonym Finance’s audit completion. Synonym Finance is a cross-chain lending and borrowing protocol powered by the Wormhole cross-chain technology stack and available in Ethereum, Arbitrum, and Optimism chains.


We Love Formal Methods

Categories