Nethermind (Formal Verification team): formal verification services for cryptography and ZK
================================================================================

Nethermind'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
Tools: Halva, sp1-lean, ArkLib, EasyCrypt, Lean 4 and Mathlib
Evidence: https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean | https://blog.succinct.xyz/nethermind-lean/

Source page: https://sorryfree.com/firms/nethermind/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13