.svg){kind=icon}
Now hiring!
We formally verify properties of your zk-circuits in the Lean proof assistant by extracting appropriate information from your zk-circuit Domain Specific Language (DSL).
We formally verify, using cutting-edge tools, that your zk-related infrastructure satisfies the desired cryptographic security properties.
We construct a mathematical model of your protocol in the Lean proof assistant and formally verify that it satisfies the desired security properties.
We are also working on developing a robust infrastructure for EVM/Yul-based smart-contract verification, relying on our in-house Clear interactive verification framework and other state-of-the-art verification tools.
RISC Zero is building its zero-knowledge virtual machine (zkVM) as a major step toward improving the security and trustworthiness of distributed applications.
Nethermind partnered with RISC Zero to develop tooling to formally verify their zk-circuit against the RISC-V semantics. Read about this ongoing work in more detail here.
Created by Matter Labs, ZKsync is a Layer 2 zk rollup, a trustless protocol that uses cryptographic validity proofs to provide scalable and low-cost transactions on Ethereum.
Nethermind partnered with Matter Labs to formally verify the honesty of the ZKsync on-chain verifier using EasyCrypt. Read about this pioneering effort in more detail here.
INTMAX is a zkRollup layer for Ethereum transfers that focuses on scalability and privacy, and comes with a mathematical specification of the underlying protocol.
Nethermind partnered with INTMAX to mechanize this specification and formally verify key security properties of the latest version of the protocol, dubbed INTMAX2. Read about this verification effort in more detail here.
We have received grants to build, in the Lean proof assistant, an executable formal model of EVM and Yul and an infrastructure for verification of Halo2 circuits.
We wrote pen-and-paper Hoare Logic proofs, verifying important properties of the Valantis protocol, such as that the Valantis contract always holds enough funds to pay its debts to its users.
We implemented an efficient automated theorem proving infrastructure for reasoning about Cairo 0 programs.
We are experts in formal methods with a shared interest in the safety and security of web3. We have extensive expertise in program verification, compiler engineering, blockchain security, cryptography, and formalization of mathematics, with publications in world-class conferences and journals in program analysis, type theory, mathematical logic, and algebra.
.svg)
.svg)
.png)
We recognize that potential applications of formal verification within the web3 ecosystem are growing rapidly. We welcome opportunities to broadening our applicability, and so if you have formal verification needs that are outside of our current scope, do get in touch and let us discuss what we can do for you.
Building blocks for the decentralized future
Nethermind © 2025
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
