ZK/SEC Research notes from zkSecurity
All posts
zk · FRI · security

Lean4 formalization of "A Simplified Round-by-round Soundness Proof of FRI"

Yoichi Hirai January 26, 2026 5 min

Round-by-round FRI soundness

How to read a cryptography paper if you are not an expert

Alice writes a cryptography paper. Charlie is not an expert. How can Charlie be sure that the paper is okay?

Alice can ask an expert Bob to review her paper. Charlie can rely on Bob's reputation to get some indirect confidence on Alice's paper. Can we do better?

There's a tool called Lean. Unlike Bob, Lean is not an expert. But it keeps asking questions until it internally completes a rigorous, small-stepped mathematical proof. The result can be published on GitHub. Usually it's called a Lean proof, or Lean formalization of the proof.

So, with the help of Lean, perhaps Charlie doesn't need to depend completely on the reputation of Bob.

What was formalized

Last October, my colleague Nico posted here Why Does FRI Work?. The post described the essence of the paper he wrote with his coauthors:

"A Simplified Round-by-round Soundness Proof of FRI" by Albert Garreta (Nethermind Research), Nicolas Mohnblatt (zkSecurity), and Benedikt Wagner (Ethereum Foundation).

Now it's formalized in Lean, except one result cited from WHIR paper about mutually correlated argument. The formalization was largely done with Harmonic's Aristotle and Claude Code.

The repository contains the Lean code for the definition and the theorems in the paper, including the proofs. The Lean type checker makes sure that the theorems are provable. The only possible room for error is misformalization: there's a possibility that the Lean statements do not exactly correspond to the statements in the paper. I need to run some examples in Lean and on paper to be completely sure that the formalization is correct. Instead I just compared the Lean code against the original paper. There are some non-critical differences between the paper and the formalization.

  • The formalization added a condition saying that the initial degree is bigger than zero. This is then used to show that the evaluation domains are nonempty. I am not sure whether this additional assumption is really needed. It doesn't matter in practice.
  • The formalization proves perfect completeness, which was not the main topic of the paper. The completeness result gives me some confidence that the formalization didn't accidentally create a verifier that refuses everything.
  • The definition of mutual correlated argument has been updated and getting stabilized over time. The formalization is based on a snapshot of the paper as of December 2025. I'm monitoring the authors' updates as well as Arklib's choices.

To be honest I wasn't expecting to find serious flaws. Indeed I didn't find any. The paper's acknowledgment mentions that Ariel Gabizon caught a mistake in an earlier draft. That gave me strong confidence in the correctness of the paper.

Lean formalization has an advantage that the correctness of the proofs is not dependent on somebody's rigor. Also, this paper formalization can be used as a specification for verifier implementations.

How it went

ItaLean 2025

I attended a workshop called ItaLean 2025. Shortly before the workshop, there were some announcements about papers getting formalized using AI agents. I asked Nico for suggestions to be formalized. He suggested his paper about FRI, so I printed it and flew to Bologna. I was showing this paper and I was talking about it. I received an API key for Harmonic's Aristotle. Many participants were trying Aristotle with their API keys that they received as participants of the workshop (Harmonic sponsored the event). I saw a mathematician saying "look at this interesting proof that Aristotle generated". That sounded promising. I asked Nico for the LaTeX source of his paper. I was ready to try Aristotle on the paper.

Formalization with Aristotle and Claude Code

The first time I asked Aristotle to formalize the paper, I waited several hours. I got some Lean code with a comment saying the budget was up. I asked Aristotle to continue and waited for several hours. I repeated this process for a while until Aristotle was not producing new statements anymore.

Then I started going back and forth between Aristotle and Claude Code. I asked Claude Code to break down lengthy proofs into lemmas, to state missing lemmas, and to add statements for completeness. I asked Aristotle to prove the conjectures that Claude Code stated. Aristotle sometimes gave counterexample to the Claude Code's conjectures. Aristotle sometimes proved the conjectures. The whole process took roughly a month and a half (I was never fully focused on this project).

For post-processing, I used Claude Code heavily. This involved removing lemmas that were never used, re-organizing lemmas into new file organization, and annotating the Lean code with references to specific locations of the paper.

What's next

The content of this project is very close to the FRI formalization project in Arklib. I think it's possible to adjust the definitions in this project so that the results can be incorporated into Arklib. The conventions in Arklib will have priority over whatever styles invented during this project.

We can also try instantiating this formalization and evaluating the soundness errors concretely.

Another direction is to prove that an implementation of a FRI verifier behaves the same way as the verifier in the paper. I'll be trying to figure out ways to get end-to-end results.

As for Charlie, he needs to learn to read Lean definitions and statements, though maybe not necessarily proofs. To be honest, he still needs to know a bit of cryptography to see that the results in Lean matter. But now, Charlie won't be completely at a loss. When some proof steps seem to be missing, the detailed lemmas in the Lean formalization can probably help fill the gap.

Thanks

This project started by Nico's initiative. He also gave me feedbacks on this post. The formalization project was possible because of access to Aristotle, which sometimes produced very involved proofs. ItaLean 2025 was great for interacting with other users and creators of Lean and autoformalization agents. Claude Code (even Sonnet 4.5) is surprisingly good at Lean. I think I'm very lucky to be around at this point in history.

The thumbnail image for this post was generated by Nano Banana Pro.

Keep reading
Latest

Variants of KZG: Part V, Multilinear Commitments with Mercury

In this final post of the series, we extend univariate KZG commitments to multilinear polynomials through Mercury. Building on Gemini, we fold half of the variables at once, use polynomial division to bind this large fold to the original commitment and reduce the remaining multilinear evaluations to a batched inner product check. We then walk through the end-to-end opening protocol. We conclude by examining its proof size, prover cost and verifier cost.

Varun Thakore · August 17, 2026

Variants of KZG: Part IV, Multilinear Commitments with Gemini

In this blog post, we extend univariate KZG commitments to multilinear polynomials through Gemini. We introduce recursive partial evaluations, derive the split-and-fold identity and express each fold as a univariate identity that can be checked using KZG openings. We then walk through the end-to-end opening protocol. We conclude by examining its proof size, prover cost, and verifier cost.

Varun Thakore · August 12, 2026

Optimizing Cryptography with AI

Many of us are using AI to generate code. Vibe coding cryptography is especially sensitive - you have to uphold strict mathematical correctness. This can lead to wrong security guarantees and soundness bugs. We will discuss what are some patterns to do it well.

Kobi Gurkan · August 11, 2026
Recommended

Why does FRI work?

This blog post explains the security intuition behind the FRI protocol, which proves that a function is close to a valid Reed-Solomon codeword. It introduces the "prover message graph," a layered structure that visualizes how correct and incorrect folds affect verification. We conclude that if too many folds are inconsistent, the verifier will likely reject, but if most are correct, the initial function must be close to a proper codeword.

Nicolas Mohnblatt · October 30, 2025

Proximity Gaps: What Happened and How Does It Affect our SNARKs

A series of recent papers just disproved the proximity gaps conjecture, which has everyone wondering if hash-based SNARKs are in trouble. We break down what actually happened using some helpful visuals. Think of it as understanding which parameter choices are safe versus which ones are now confirmed to be risky. The post walks you through the different security zones (proven safe, conjectured safe, and definitely not safe), explains how these new results connect to other open math problems, and shows what it means for real-world SNARKs in terms of proof sizes and performance trade-offs.

Nicolas Mohnblatt · November 14, 2025

An Introduction to Interactive Theorem Provers

Kevin Buzzard, a mathematician with a cautious view on human-checked proofs, found solace in interactive theorem provers, which verify mathematical proofs much like type-checking in programming. We explore how these tools, which are gaining traction in fields like applied cryptography, ensure rigorous and reliable proofs. With Lean as our focus, you'll discover how to dive into this fascinating world, see a proof in action, and learn how this technology is revolutionizing areas like zero-knowledge virtual machines. Curious about building rock-solid, machine-verified proofs? Check out our beginner-friendly guide!

Marco Besier · February 04, 2025
More to explore

Announcing the S-two Book

We're thrilled to share our collaboration with Starkware on the S-two book. If you're curious about writing AIRs with the S-two prover, implementing Cairo AIR in S-two, or how Circle STARKs are utilized, this post is for you. Dive in to explore these insights and deepen your understanding of these fascinating topics.

Jason Park, Varun Thakore · November 11, 2025

Comparison of formal verification frameworks for arithmetic circuits

A hands-on comparison of formal verification frameworks for arithmetic circuits, evaluating those in the ACL2 Book (r1cs, PFCS), acl2-jolt, Garden (Rocq), zk-lean, sp1-lean, and Clean. Each framework is tested on reproducibility, available examples (from basic field elements to RISC-V VM instructions), and practical verification tasks including the IsZero and weighted-sum circuits. The evaluation includes both human and Claude Code's ability to work with each framework, revealing insights about installation difficulty, proof automation capabilities, and the maturity of publicly available examples. This post maps the current landscape of formally verified ZK circuits and discusses what's coming next in this rapidly evolving field.

Yoichi Hirai · November 19, 2025

The zero-knowledge attack of the year might just have happened, or how Nova got broken

Last week, a surprising paper revealed a major vulnerability in Microsoft's Nova, a leading zero-knowledge proof (ZKP) system, that showcased a false computation with a valid proof. This discovery is especially intriguing given the complexity and robustness typically associated with ZKP systems. We had just launched our company to tackle bugs in ZKP frameworks, and while we anticipated issues, complete breakdowns of systems themselves are rare. Nova's issue revolved around cycles of elliptic curves, showing how small implementation oversights in complex cryptographic systems can lead to significant errors. This post dives into the intricate mechanics of Nova and the discovery process, offering a fascinating glimpse into why rigorous specifications are crucial in cryptography.

David Wong · July 02, 2023