Welcome to the Runtime Verification blog

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

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!

Audit competitions have surged in popularity recently, with numerous platforms vying to connect projects with independent security researchers. The premise is straightforward: organizations offer a cash prize to attract auditors eager to scrutinize their code for vulnerabilities. While cost-effective, the evolving ecosystem necessitates a closer examination of the drawbacks inherent in relying solely on audit contests.

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.

In our previous blog post, where we introduced our new ERC-4626 test suite, we briefly described the specifications of an ERC-4626 vault and how we can leverage property tests to check that the vault satisfies the required properties stated in the EIP-4626. For this blog post, we use Version 2.2.0 of the ERC-4626 test suite and ERCx4626Mock0 to guide readers through and provide a visual reference.

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

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.

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.

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.

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.

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.

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.