Protocol verification
Proving that protocols hold under adversarial conditions
Blockchain systems autonomously manage assets of significant monetary value, so their proper operation and their resilience against adversarial behavior are the whole game. Making sure they are secure is of paramount importance.
Consensus protocols
Fundamental to every blockchain-based system is the correctness of its underlying consensus protocol, which covers two things at once: a mechanism for decentralized selection of one or more block proposers for a round, and a mechanism for reaching decentralized consensus on the single block to append to the chain.
The problem
Designing and implementing blockchain systems, consensus protocols in particular, is intrinsically hard. Every time the protocol evolves it introduces additional interactions, and ensuring correctness gets harder again. Ad-hoc designs built on informal descriptions produce buggy and vulnerable implementations, and there is always the gap between the protocol design and the actual implementation.
Our approach
A formal specification first, then a proof that the design meets it.
Our approach to protocol verification is centered on formal methods. First we build formal specifications of the protocol's design and of its properties, the latter representing the requirements the design is expected to satisfy. Then we verify mathematically that the design meets them.
Using the K framework, that specification is formal and executable. Executable specifications let us run simulations and animate systems, which is useful for prototyping and debugging designs during development, and they serve as a reference implementation for model-based test generation. The same specification is then immediately available to reachability, model checking and theorem proving tools for other forms of formal analysis.
Work to date
Benefits
Apply formal methods as early as the design allows.
- Uncover fundamental errors that would otherwise go undetected.
- Employ your protocol's high-level specification to document and prototype the design.
- Generate efficient implementations and tests for your protocol.
- Formally verify your protocol's properties.
- Increase confidence in the correctness and security of the decentralized system powered by your protocol.
From the blog
Writing on verification.
Hardening Linux's C Code: A Rewrite-and-Verify Loop
While testing our reusable C-to-Rust verification workflow on the Linux UVC parser, we found a real integer-overflow bug and joined the upstream fix. The workflow combines a safe Rust rewrite, differential fuzzing against the kernel C, and Lean proofs of the key safety properties behind CVE-2024-53104.
Verifying Linux's Rust Code: From Binder To Lean 4
Android's Binder driver parses attacker-controlled bytes on three billion devices. As part of our formal verification work targeting Linux kernel, we proved that its deserializer never panics on any userspace input, all machine-checked end-to-end from production Rust through Charon and Aeneas into Lean 4.
When the Software Holds but the Money Leaves Anyway
A technical analysis of the April 2026 KelpDAO bridge incident, in which $292M was lost despite every audited on-chain component performing exactly as specified, with the actual compromise occurring in the off-chain operational layer that surrounded them.
From Rust Code to Mathematical Proof: How We Verify Safety-Critical Rust
Runtime Verification applies formal methods to cryptographic and safety-critical software. We turn production Rust into machine-checked Lean 4 proofs of correctness, no sorry left behind.
Protocol verification team
The full teamDesigning a protocol that has to hold under attack?
Work with us