Ethereum Foundation
Revm formal specification - Rust / EVM
A public formal specification for Revm, the Rust implementation of the Ethereum Virtual Machine.
Verified using our tool rocq-of-rust
Formal verification since 2021
Formal Verification for Web3
We secure critical components in Rust, Solidity, and OCaml with formal verification workflows that follow code changes.
- Formal verification audits for high-risk code paths
- Ongoing proof maintenance as implementations evolve
- Consulting, tooling, and training for engineering teams
revm/proofs/EvmStep.vRocq ✓
(* Revm — EVM step preserves invariant *)
Theorem step_preserves_invariant :
forall (pre post : State) (op : Instruction),
step pre op = post →
valid_state pre →
valid_state post.
Proof.
(* 124 lines · machine-checked *)
Qed.Public evidence
Public proof reports
Public reports show the kind of proof work we deliver for blockchain infrastructure, smart contracts, and cryptographic systems.
Ethereum Foundation
ZK verification reports
Verification work on Keccak, branch equality, and LLZK-related proof artifacts for zero-knowledge systems.
Verified using our tool garden
Sui
Move type-checker - Rust
Formal verification of part of the type-checker for the Move language, focused on correctness-critical infrastructure code.
Smoo.th
Elliptic curve library - Solidity
Formal verification work for a Solidity elliptic curve library where small arithmetic mistakes can invalidate protocol assumptions.
Verified using our tool rocq-of-solidity
Aleph Zero
Source-level verification tooling - Rust / Solidity
Source-level verification work that grew our Rust and Solidity toolchain, supporting maintainable proofs on production code.
Verified using our tools rocq-of-rust and rocq-of-solidity
Tezos
Layer 1 verification - OCaml
Verification work on parts of the Tezos implementation, leading to our long-running OCaml verification toolchain.
Verified using our tool rocq-of-ocaml
Partners
Web3 security patners
What you can buy
Formal verification engagements
We scope work around the small parts of a system where proof adds the most value.
Formal verification audit
A focused engagement for a code snapshot where a small set of high-value properties needs stronger evidence than tests can provide.
- Choose the component and properties to verify
- Build machine-checked Rocq/Lean proof artifacts
- Deliver a report that engineering teams can inspect
Ongoing verification subscription
A recurring workflow for teams that need proofs to remain useful as requirements, code, or dependencies change.
- Track changes in selected critical components
- Replay and update proofs during release work
- Keep verification cost focused on what changed
Consulting, tooling, and training
Expert support for teams adopting formal methods or connecting production languages to Rocq/Lean proof workflows.
- Design specifications around real engineering requirements
- Build source-level translation and proof tooling
- Train teams to maintain proof artifacts over time
Where we fit
Built for Web3
Smart contracts, protocols, and cryptographic infrastructure where bugs are public, costly, and immutable once deployed.
Smart contracts and protocols
Token logic, AMMs, bridges, governance, and protocol-level invariants where a single bug can drain funds or break consensus.
Rust, OCaml, and Solidity
Source-level verification for the production languages of Web3 using our translation tools and Rocq/Lean proof engineering experience.
Cryptography and ZK systems
Arithmetic, constraint systems, hash functions, and circuit-adjacent code, where implementation errors can invalidate security arguments or break interoperability between proving systems.
Reusable proof workflows
Open-source tooling and maintainable proof structures that make verification work replayable rather than one-off documentation.
Always advancing
Pushing the formal methods frontier
Verification is only as strong as its scope and the precision of its specifications. We continuously innovate in both areas to provide the most extensive security coverage we can.
How projects work
A narrow proof target, then replayable evidence
- Identify one component where failure would be costly
- Define the precise safety or correctness properties worth proving
- Connect the source code to Rocq/Lean proof workflows
- Deliver specifications, proof artifacts, and a verification report
- Keep proofs aligned as the implementation evolves
FAQ
What do buyers get at the end of a project?
A focused report, specifications, and machine-checked Rocq/Lean proof artifacts for the properties agreed at the start of the engagement.
Do you verify an entire codebase?
Usually not at first. The best starting point is a narrow component where failure would be costly: a control module, protocol component, cryptographic routine, type-checker rule, or interface boundary.
How does this fit with testing and review?
Formal verification complements tests, audits, and code review. It gives machine-checked evidence for selected properties that are hard to cover exhaustively with tests alone.
Which parts of a Web3 stack do you verify?
Smart contracts, virtual machines, type-checkers, protocol logic, and cryptographic or zero-knowledge components.