Category: verification
With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review
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).
External Computation with Kontrol: Leveraging Foundry Execution for Formal Verification
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!
Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs
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.
Enhancing Stable MIR with Serde Serialisation
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).
Formal Verification Lore: Intuitive Intro to Why We Can Prove Programs Correct
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.
Introducing KMIR: concrete and symbolic execution of Rust MIR
Runtime Verification is excited to announce the open public alpha of KMIR. KMIR defines the formal operational semantics of the Middle Intermediate Representation (MIR) of Rust in K, giving developers access to the K framework tool suite for MIR programs.
Using Foundry to Explore Upgradeable Contracts (Part 1)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Warning: Code Can Be Explosive
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Foundry: Gen 2 of Ethereum Tooling
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Dexter 2’s Formal Verification
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
