Formal verification services

Formal verification offers the strongest possible correctness and security guarantees to the web3 ecosystem, in which smart contracts and protocols directly handle billions of dollars in assets, and exploits often lead to immediate and irreversible financial losses.

Solutions across three main areas

zk-circuit

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).

zk-related cryptography

We formally verify, using cutting-edge tools, that your zk-related infrastructure satisfies the desired cryptographic security properties.

Protocol modelling

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.

We are RISC Zero’s verification partner

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.

We are the first to formally verify a real-world zk-verifier

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.

We prove security of cutting-edge protocols

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.

Formal verification, specification and tooling

We offer a range of formal verification and specification categories, with varying levels of security. Our team will guide you to a formal verification and specification service that best suits your projects needs.

Other clients

Ethereum Foundation

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.

Valantis

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.

Past and current clients

Starkware

StarkWare is using STARK proofs to bringing scalability, security and privacy to a blockchain near you.

ZKLend

zkLend is a protocol combining zk-rollup scalability, superior transaction speed, and cost-savings with Ethereum's security.

Our team

The Nethermind Formal Verification team comprises experts in formal methods who share a particular interest in the safety and security of the web3 ecosystem.

The team members have extensive expertise in program verification, compiler engineering, blockchain security, cryptography, and formalization of mathematics, and have authored publications in world-class conferences and journals in program analysis, type theory, mathematical logic, and algebra.

Get in touch!

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.

Collaborating on this project

Julian

Sutherland

Ilia

Vlasov

František

Silváši

Collaborating on this project

Julian

Sutherland

Ilia

Vlasov

František

Silváši