Nethermind (Formal Verification team)
Nethermind's formal verification team works in Lean 4 and EasyCrypt. It builds CertiPlonk, a Plonky3 extraction and verification framework now applied to OpenVM, Brevis Pico and Poseidon2, co-developed sp1-lean with Succinct, built the earlier Halo2 extractor Halva (finding a critical bug in Scroll's deprecated Keccak circuit), maintains an ArkLib FRI fork and a Lean EVM model (EvmYul), and produced the first honesty proof of a production ZK verifier for ZKsync in EasyCrypt.
- Website
- https://www.nethermind.io/formal-verification
- Headquarters
- London, United Kingdom
- Focus
- Lean and EasyCrypt verification: CertiPlonk (Plonky3, zkVM chips), sp1-lean, Halva (Halo2), ZKsync verifier honesty proof
- Index position
- #4 of 11
Services
- Halo2 and Plonky3 circuit verification in Lean
- zkVM chip verification (SP1, Pico, OpenVM)
- EasyCrypt proofs for verifiers and protocols
- EVM semantics and equivalence proofs
Frameworks this firm builds or uses
CertiPlonk, sp1-lean, Halva, ArkLib, EasyCrypt, Lean 4 and Mathlib.
Public evidence
- CertiPlonk introduction (2025-11-14)
- From CertiPlonk to zkVMs: OpenVM, Pico and Poseidon2 (2026-07-03)
- SP1 Hypercube Lean verification (2025-10-09)
- Halva and the Scroll Keccak finding (2025-07-02)
Best fit
Choose Nethermind for Plonky3 circuits and zkVM chip verification (CertiPlonk, sp1-lean), for Halo2 extraction, and for EasyCrypt proofs of on-chain verifiers, especially in Ethereum L2 stacks.
Other firms on this index
zkSecurity, Galois, Veridise, Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software