Nethermind (Formal Verification team)
Direct answerNethermind's formal verification team works in Lean 4 and EasyCrypt. It built Halva for Halo2 (finding a critical bug in Scroll's deprecated Keccak circuit), co-developed sp1-lean with Succinct, 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: Halva (Halo2), Plonky3 circuits, SP1 chips, 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
Halva, sp1-lean, ArkLib, EasyCrypt, Lean 4 and Mathlib.
Public evidence
Best fit
Choose Nethermind for Halo2 or Plonky3 circuits and for zkVM chip verification, 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