Formal verification for high-stakes blockchain and zero-knowledge systems

Audits and testing check for issues someone thought to look for. They can show that bugs exist but never prove that none remain. Formal verification uses machine-checked proofs to show a system behaves according to formally specified correctness properties across every possible execution, which is a stronger assurance for the properties that get verified.

No, formal verification does not replace an audit. It establishes that a system meets the correctness properties it was specified against. Problems outside those specifications, such as access-control misconfigurations or economic design flaws, still need an audit and broader security review. The two are complementary.

A proof establishes that a system matches the correctness properties it was specified against, across all executions those specifications cover, checked by machine rather than by example. The strength of the result depends on the properties specified and the assumptions they rest on, which is why scoping and specification development are central to every engagement.

Each engagement starts with detailed analysis of the system and the properties it needs to hold, followed by threat modeling, specification development, verification planning, formal modeling, and machine-checked proof development. Specifications come from direct technical discussion with the team building the system, not from informal documentation.

Formal specifications, correctness proofs, protocol models, a verification report, remediation guidance, and, in certain cases, reusable tooling.

Work spans zk proof systems and verifiers, zk circuits, zkVMs, cryptographic protocols, blockchain protocols and distributed systems, execution environments, and high-value smart contracts. We are working with several ecosystems, such as Ethereum, Aptos, and ZKsync, and clients such as Succinct, Axiom, Brevis, RISC Zero, and INTMAX.

The Formal Verification team primarily uses Lean, with verification work across Halo2, Plonky3, Circom, and EVM/Yul, supported by in-house infrastructure including CLAP, CertiPlonk, Halva, Surveyor, and ArkLib.

The team's work centers on Ethereum and the EVM, Starknet, and the proof systems and zkVMs used across the ecosystem. Coverage is defined by the proving system and execution environment rather than a fixed chain list, spanning EVM and Yul execution, Halo2 and Plonky3 circuits, zkVMs such as SP1, OpenVM, and RISC Zero, and protocols like ZKsync and INTMAX.