.svg){kind=icon}
Now hiring!
“Program testing can be used to show the presence of bugs, but never to show their absence.”
Edsger Dijkstra
Zero-knowledge systems and blockchain cryptographic protocols increasingly operate as production financial and computational infrastructure. In these environments, correctness failures can have significant security and financial consequences.
The team applies hard formal methods, protocol modeling, and interactive theorem proving to provide strong correctness assurances for production cryptographic systems. The team works closely with the Ethereum Foundation to secure the cryptographic foundations of the L1 proving transition.
The work spans across zk proof systems, zkVMs, protocol verification, execution semantics, and verification infrastructure for production blockchain systems.
Formal verification uses machine-checked proofs to demonstrate that systems behave according to formally specified correctness properties.
In these environments, subtle implementation errors, invalid constraints, verifier inconsistencies, or protocol-level failures may not be discoverable through conventional testing or security review alone.
Formal verification complements audits, testing, and security engineering by providing stronger assurances for systems where correctness requirements are unusually high.
Zero-knowledge systems
Cryptographic protocols
Blockchain execution environments
Distributed systems
Systems securing significant value
Lean
Halo2
Plonky3
Circom
EVM / Yul
CLAP
CertiPlonk
Halva
Surveyor
ArkLib
Bluebell
The work spans zero-knowledge systems, cryptographic infrastructure, blockchain protocols, and execution environments.
Verification of zk circuit correctness and proving-system behavior across Halo2 and Plonky3 systems. Includes work on CLAP, a Lean-based zk circuit compiler carrying correctness assurances from source specifications through generated constraint systems.
Formal verification of zk proof systems, verifiers, and their implementations. Includes development of the FRI formalization in ArkLib and ongoing work toward STIR/WHIR formalization.
Mathematical modeling and verification of blockchain protocols and distributed systems.
Reusable verification infrastructure, formal semantics, and theorem-proving tooling for Ethereum and zk systems.
Formal reasoning about smart contract execution behavior for systems requiring stronger correctness assurances.
A significant portion of the work focuses on reusable verification infrastructure rather than one-off engagements. The team is building formal methods infrastructure for Ethereum and the broader ecosystem.
Every engagement is shaped around the specific properties, assumptions, and threat models of the target system. There is no template. The team works directly with each client to identify the correctness and security properties that matter most, then scopes a verification effort to those failure modes.
The methodology favors the strongest available techniques over the most convenient ones. Specifications are derived from deep technical discussions with teams rather than informal documentation.
The objective is mathematical certainty, not empirical confidence accumulated from test cases.
Representative verification work across zk systems, execution environments, protocol verification, and formal methods infrastructure.
First formal proof of honesty for a production zk verifier implementation using EasyCrypt.
EasyCrypt
•
zkSync
Verification work across zkVM systems including SP1, Pico, and OpenVM.
Succinct
•
Brevis
•
Axiom
Formal semantics of the EVM and Yul in Lean for the Cancun hard fork, passing 99.99% of official Cancun execution tests.
Ethereum Foundation
•
ArkLib
•
Yul
First executable model of the FRI protocol in Lean, with formalization of STIR and WHIR in progress. Building formally verified implementations of these key cryptographic protocols to secure Ethereum during the L1 proving transition.
Ethereum Foundation
•
ArkLib
•
Axiom
Framework for extracting and formally verifying Plonky3 zk constraints in Lean without modifying developer workflows.
Plonky3
•
Lean
Lean-based infrastructure for verifying Halo2 circuits used in production zk systems.
Halo2
Lean-based zk circuit compiler carrying correctness assurances from source-level specificationsthrough generated constraint systems.
Aptos
•
Lean
•
zkDSLs
Formal verification of key security and correctness properties for the INTMAX2 protocol.
INTMAX
•
Distributed Protocols
This is a research project that Nethermind is currently conducting on behalf of Lido.
zk proof systems & zkVMs
Blockchain protocols
Cryptographic infrastructure
Execution environments
High-value smart contract systems
Systems secure significant value
Protocol correctness is foundational
Cryptographic assumptions are critical
Infrastructure dependencies expand
Failures are difficult to detect through testing alone
Every engagement is scoped to the system in front of the team. It begins with detailed analysis of the target and its threat model, moves through specification and verification planning, and into formal modeling and machine-checked proofs. Each phase is shaped around the failure modes that matter most for that system.
Reusable zk verification infrastructure
zkVM verification systems
Probabilistic program logics
Proof-system verification
Post-quantum cryptography
Contributions also include formalization efforts related to post-quantum cryptography and emerging cryptographic standards. Formal verification is expected to become increasingly important as zero-knowledge systems and cryptographic infrastructure mature into foundational financial and internet infrastructure.
How formal verification differs from an audit, what it proves, and what an engagement produces.
The Leading Engineers of Blockchain Infrastructure
Nethermind © 2026
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)