The future of security is formally verified cryptography.

But who verifies the formal verification?

We do!

Introduction

Formal verification is a powerful tool for proving properties about software, but the dirty secret of formal verification is that it is software too, and like all software, it can have bugs. Whenever someone claims to have done formal verification of a system, that claim does not exist in a vacuum: all formal verification is under assumptions. Either formally stated mathematical assumptions, definitions of security, idealizations of the system, or that equivalence between the formal specification and the implementation is correctly enforced. So although formal verification greatly simplifies the process of verifying correctness of software, by allowing humans (and machines) to inspect higher-level properties of the system instead of inspecting low-level details, the formal verification itself requires auditing. This is exactly what we have spent 3 weeks doing on the recent Ironwood formalization, working with the Zakura team on an audit funded by Tachyon Foundation.

Common Mistakes

Before we explore the Ironwood formalization, let's discuss some of the general pitfalls of formal verification. Going, roughly, from easiest to avoid, towards harder to avoid.

Kernel Bugs. There has been much talk about the recent bug in the Lean kernel. These are inconsistencies in the Lean type system that allow you to prove a contradiction, which in turn allows you to prove any property you want. This has become a rite of passage for interactive theorem provers, notably Rocq/Coq has had a number of these. They have impact on e.g. formally verified autoresearch, such as better.codes and zk.golf, where, potentially malicious, parties write the proofs. However, for "honest" formalizations of protocols/implementations, like Ironwood, the practical impact is non-existent: upgrading the Lean kernel will detect the fault and humans/agents do not "accidentally" write proofs that would exploit Kernel bugs. As an analogy, this is not dissimilar to finding a Rust program that miscompiles for a specific rustc version, but those are rare, and unless you seek them out, you are unlikely to encounter them.

Non-Standard/False Assumptions. In Lean (and other theorem provers) you can introduce new assumptions; the first relevant security question is whether a formalization relies on such non-standard assumptions or sorry that essentially means "trust me on this without a proof". For most formalization tasks new assumptions are not needed, however, LLMs sometimes love to introduce them. If the formalization does rely on non-standard assumptions, the validity of these must be verified outside the theorem prover (Lean) by human inspection (and by e.g. referring to a paper). Mechanically checking for sorryAx and other unintended assumptions is very easy, and should be done in continuous integration. Avoiding this mistake is largely table stakes, for LLM-written proofs, tools such as comparator can be used to ensure that the agent does not change theorem statements or assumptions, when it thinks the proof is too tough...

Security Definitions. If you prove security, the next question is "what do you mean by security?" In Lean this means stating a formal security definition, for instance:

"If the verifier (some concrete Lean code) accepts with probability $\epsilon$, then the extractor (some concrete Lean code) can recover a witness with probability $\delta$".

Because they need to be formally defined, it means that we know exactly how security is defined, which is great, but it also means that the potential for finding "technical edge cases" is greater. Classic mistakes include proving an implication e.g. if $A$ then $B$, but where $A$ is always false for an unintended reason, relying on a hypothesis which is false or proving probability bounds which can be made vacuous. In addition, there are sometimes informal assumptions on proofs, for instance, in a "proof of knowledge" the extractor (some Lean function) may be assumed to be efficient.

Formalization $\Leftrightarrow$ Implementation Correspondence. Lean can only reason about Lean code. So after proving properties about the Lean code, we need to relate the Lean code to the deployed implementation. There are different ways to achieve this, for instance:

• You can model the semantics (behavior) of the implementation language (e.g. Rust) inside of Lean, then use a tool (e.g. Aeneas) to convert the implementation code into Lean. Then you (or your agent) prove equivalence between the lifted Rust implementation and the Lean implementation. There is some trust introduced here: you need to trust that the modelling of the language is correct and that the tool is correctly converting the implementation code into Lean.

• You can export values (so-called "fixtures") from the real implementation, then cross-check them against the values computed by the implementation inside the formalization. Here you need to ensure that the fixtures capture all the relevant parts of the implementation, if you verify something about the Lean reference, but which is not captured by a fixture, that does not carry over to the implementation. For Ironwood, the fixtures consist of exporting the circuits and final verifier checks (multi-scalar multiplication) to check that the circuits and the Lean reference verifier are consistent with the implementation.

Ironwood

Ironwood is a formalization of the verifier in the Halo2 proof system, along with the Ironwood (fixed Orchard) action circuit, responsible for verifying the spending of a note.

Circuit Formalization. The circuit is formalized in the Clean framework, where knowledge of a witness for the low-level Plonkish constraints is proved to imply knowledge of a witness for the more high-level spending relation. To model the computational assumptions inside the circuit, the extraction theorems follow a "valid or break" pattern where either a valid witness is recovered, or a witness showing a violation for a computational assumption is recovered (e.g. a collision for the "Sinsemilla" hash). The consistency between the deployed circuits and the formalization is checked by having the Rust implementation export the verification key, which is then recomputed on the Lean side (from the Clean circuit) and checked for equality.

Verifier Formalization. The Halo2 proof system is instead modelled as an interactive proof system (prior to Fiat-Shamir) in the algebraic group model (AGM), meaning that for every group element, the (potentially unbounded) prover produces, a representation (a linear combination of the URS elements) is provided. The extractor recovers either a valid witness for the circuit relation (by solving a linear system in the representation) or a non-trivial discrete log relation (a non-zero linear combination of the URS elements resulting in the identity element). The consistency between the deployed verifier and the formalization is checked by exporting the final verifier MSM (which batches all the checks) for a number of valid/invalid proofs from the Rust side, then recomputing the MSM component on the Lean side and checking for equality.

These two components, and their respective proofs, are then combined to produce a set of "capstone theorems" which make statements along the lines of:

"the extractor recovers a valid witness for the (high-level) action relation (a spending witness) or a non-trivial discrete log relation"

The Audit

This brings us to our audit of the Ironwood formalization. The goal of the audit was not to verify that Ironwood is correct, but the stronger goal of verifying that the formalization itself is robust against whole classes of potential issues in the implementation. Instead of finding bugs in the honest implementation, we went looking for malicious implementations that would still pass the formalization, in other words, ensuring that, within the scope of the formalization, deliberately breaking the implementation would cause one or more "Capstone Theorems" to fail: meaning that we could not prove security of a broken implementation according to the security definitions. This includes attempts to:

• Inject faults into the circuits on the Rust side.
• Make sure the fixtures are correctly exported and imported into Lean.
• Break the verifier itself (within the boundary of being "algebraic").
• Circumvent the security definitions by making them vacuous to prove security of a broken scheme.
• And much more.

During the audit we did not find any ability to bypass the formal verification within the scope, beyond the known limitations of the formalization itself. Conversely, we found a number of interesting observations at the "periphery" of the formalization, things that are not strictly within the scope of the formalization itself, but ways that a fault in the implementation, honest or malicious, could go undetected by the formalization.

Our full report is available at reports.zksecurity.xyz.

Or read Zakura's post for more details.

Conclusion

Formal verification is a powerful tool, it can ease our burdens and let us sleep much better at night, but it is not the end of all security considerations. The guarantees provided by a good formal verification are far stronger than those provided by traditional security audit of the same codebase. Because it provides a positive guarantee, as opposed to a negative one for a traditional security audit, it certifies that the code is free from entire classes of issues. But not every formal verification is equal, in the same way that not all other software is equal: writing a formal verification (even with AI) still requires both domain expertise (in e.g. zero-knowledge proofs) and technical expertise (in e.g. Lean), to understand the assumptions and properties being verified. It's been a great pleasure to work with the Zakura team to "pressure test" their Ironwood formalization. Clearly a lot of thought and work has gone into it, even though it was undertaken in a short timespan.

If you are interested in formal verification, or would like another pair of eyes on your formalization, reach out to us. We do both audits and development, we can also help you get started with formal verification.