Formally Verifying OpenVM's Keccak and SHA-2 Circuits

Alongside the OpenVM 2.0 release, we expanded OpenVM’s formal verification coverage to include the Keccak and SHA-2 extensions, proving in Lean that each circuit correctly constrains the relevant hash computation. These Lean proofs provide programmatically checkable certificates that the corresponding OpenVM circuits are correct for all input values and do not omit any necessary constraints, giving a stronger correctness guarantee than is possible with traditional security methods like unit testing or fuzzing.

Our use of formal verification is a response to the emerging threat landscape. As described in our prior post on the vulnerability we found in the zero-knowledge (ZK) proof system powering Starknet, AI is changing how software gets attacked: models can now read large codebases, reason about how they behave, and surface exploitable flaws faster and at greater scale than traditional defenses can keep up with.

We chose to formally verify OpenVM’s Keccak and SHA-2 circuits because the hash functions they implement are among the most security-critical components in the system and are frequently used in cryptographic infrastructure across the internet and Ethereum. In a ZK proof system like OpenVM, these hashes are not executed directly but constrained as circuits. Any gap between a circuit and the function it intends to constrain can let a malicious prover produce a valid-looking ZK proof of an incorrect result, making the correctness of these circuits paramount for the security of the overall system.

In the rest of this post, we explain what formal verification entails, how we verified OpenVM’s Keccak and SHA-2 circuits, and how it translates into concrete security guarantees. The formal verification artifacts are available on GitHub.

The Security Benefit of Formal Verification

Conventional software assurance is built around finding defects: testing runs a system on selected inputs and checks the outputs, review has engineers inspect the code, and software security products enable more automated and comprehensive detection. Formal verification provides a categorically different assurance by proving mathematically that a program satisfies a stated property on every possible input, so entire classes of bugs can be ruled out.

This is especially useful for ZK circuits like those in OpenVM’s Keccak and SHA-2 extensions, which have a failure mode unlike that of conventional software: subtle omitted constraints can be easily missed by human auditors and cannot be detected through unit testing. When a circuit is underconstrained, it can accept a trace that encodes the wrong hash, enabling a malicious prover to certify an illegitimate execution. That threatens the core utility of systems like OpenVM, where a verifier trusts the proof instead of re-executing the program.

This is not a hypothetical risk. In June 2026, Zcash disclosed exactly such a flaw in the circuit behind Orchard, one of its shielded pools: a missing constraint in the double-spend check could let a prover spend the same shielded note repeatedly, minting unlimited counterfeit ZEC, a token with an $8 billion market cap at the time. The flaw had been live since Orchard launched in 2022, surviving four years of testing and audit. It was surfaced by one of Anthropic’s frontier models under a targeted review, which fortunately was carried out by a security researcher rather than a malicious attacker.

Our Approach to Formal Verification

We approach formal verification in three key steps:

• Extraction: Deriving a formal model of a system in Lean from the production implementation to enable us to reason about it formally.
• Specification: Establishing a formal reference in Lean for the system’s intended behavior, either developed in-house or taken from an independent authoritative source.
• Proving: Proving functional equivalence between the extracted model and the formal specification, with the resulting Lean proofs checked programmatically.

These processes use the Lean proof assistant and take the corresponding Lean kernel and comparator as a trusted base on which extraction, specification, and proving take place. The extraction and specification are trusted pieces of the verification and require human review to ensure that they correctly represent the intent of what we are verifying. Once this is done, proof verification is programmatic using the Lean kernel, meaning that correctness can be assessed without human experts.

To generate the proofs, we built an agentic formalizer based on the latest frontier models and a custom harness for verification. To guard against reward hacking and other potentially adversarial AI behavior, we constrain our agent with theorem integrity checks enforced by the Lean comparator. This enables us to use long-running agentic processes to generate Lean proofs without compromising correctness. The result is a process that can scale to large cryptographic systems like OpenVM’s circuits, which were historically costly and time-consuming to formally verify.

How We Verified OpenVM's Keccak and SHA-2 Extensions

We proved one theorem for each OpenVM circuit: if an execution's trace satisfies the circuit's constraints, then the circuit computes exactly the hash specified by an independent reference.

We programmatically extracted each circuit's low-level polynomial constraints directly from its production implementation in Rust into Lean to produce a Lean model of the Keccak and SHA-2 circuits. Our extraction treats all polynomial constraints uniformly and ensures that the Lean representation of the circuits is faithful to what OpenVM uses in production.

We developed reference specifications from standards written by the National Institute of Standards and Technology (NIST) and imported them into Lean. For the Keccak circuit (which implements keccak256 but uses the same permutation as SHA-3), we used the Keccak-f[1600] permutation with the round constants and rotation offsets of NIST FIPS 202. For the SHA-2 circuit, we used the SHA-256 standard as specified in NIST FIPS 180-4, with its round constants, initial hash values, and rotation amounts. We carefully audited the correspondence between each reference specification in Lean and its published FIPS standard.

We then used our agent to produce Lean proofs that the extracted circuits for Keccak and SHA-2 satisfy the reference specifications, ruling out the entire class of vulnerabilities caused by missing circuit constraints. The resulting proofs were checked by the Lean kernel and assessed by a Lean comparator against their reference statements to rule out statement tampering. Of course, the validity of this verification rests upon the correctness of the trusted computing base, comprising the extraction from ZK circuits to Lean, the reference specification, and the Lean kernel and comparator themselves.

What’s Next

Formally verifying the Keccak and SHA-2 extensions is the first step in our ongoing program to secure OpenVM with frontier defense techniques built for a threat landscape now shaped by AI. For mission-critical components like these hash functions, testing or searching for failures is no longer enough. Instead, we need formal verification to provide a security guarantee that holds no matter how powerful the attackers’ tools become.

Though these guarantees are powerful, producing them is extremely complex and requires deliberate engineering throughout the process: finding an independent specification, implementing extraction that is faithful to the production implementation, and designing robust verification to enforce theorem integrity and prevent any hidden gap or disallowed axiom.

Done correctly, formal verification offers the highest assurance level possible for software. Stay tuned for more work from us in this direction.