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.
Semantic Equivalence with the K Framework
KEQ proves migrated code behaves exactly like the original, on all inputs — from small C/Rust examples to SHA-256 implementations in OpenSSL and RustCrypto.
Verifying the Linux kernel's isolation code: a policy bypass in io_uring's sandbox filter
A policy bypass in io_uring's sandbox filter, found by writing down what the filter should see. The bug, the reproducer, and a fix in mainline in a day.
Formally Modelling Optimism's Supernode: A Dafny Model, an AI Reviewer, and What They Achieved Together
Optimism's Supernode decides which cross-chain messages are valid and advances the cross-safe frontier: get it wrong in one direction and a chain builds on invalid state; wrong in the other, and the whole cluster stalls. This post covers a hand-written Dafny model of its core logic we built during a 10-week audit extension, and how we used it as the basis for AI-assisted fuzzing and comparison against the Go implementation.
Verifying the Linux kernel's isolation code: user namespaces, a proof, and a patch
We verified a core piece of the Linux kernel's container isolation code in Lean 4, and writing the spec turned up a parsing bug we've sent a fix for upstream. We also learned where AI speeds up proofs and where it gets the specification wrong.
Protocol verification team
The full teamDesigning a protocol that has to hold under attack?
Work with us