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 III, Multilinear Commitments with Zeromorph

In this blog post, we extend univariate KZG commitments to multilinear polynomials through Zeromorph. We introduce the univariatization map, encode the multilinear quotient identity as a univariate identity, and explain why the quotient encodings require degree checks. We then show how Zeromorph batches these checks into a single degree-bounded KZG opening and walk through its end-to-end opening protocol. We conclude by examining its proof size, prover cost, and verifier cost.

Varun Thakore · August 04, 2026

Variants of KZG: Part II, Multilinear Commitments with PST

In this blog post, we extend the ideas behind univariate KZG commitments to multilinear polynomials through the PST commitment scheme. We derive the multilinear quotient identity, explain how PST commits to and opens multilinear polynomials using a specialized multilinear setup and walk through its opening protocol. We conclude by examining the proof size, prover and verifier costs, and the limitations that motivate other multilinear polynomial commitment schemes.

Varun Thakore · July 28, 2026

Threshold ECDSA: Building CGGMP from scratch

A step-by-step build of CGGMP, an n-of-n threshold ECDSA scheme where parties jointly produce a signature without ever reconstructing the private key. We start from the multiplicative-to-additive (MtA) protocol and a semi-honest version of the signing protocol, then harden it into a maliciously secure one by layering in zero-knowledge proofs at each step. Along the way we cover the auxiliary Ring-Pedersen and Paillier parameters and the proofs that make them safe to use.

Samuel Tang · July 27, 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

Reproducing and Exploiting ZK Circuit Vulnerabilities

Check out our latest blog post where we dive into the world of Zero-Knowledge Proof (ZKP) vulnerabilities, sharing our insights from replicating known ZK circuit weaknesses. We’ve launched a GitHub repo with detailed scripts to help you understand, reproduce, and learn from these vulnerabilities. Discover how this hands-on approach aids in grasping attack vectors, testing fixes, and enriching educational resources. Whether you're a researcher or a developer, this post is packed with info to enhance your knowledge and skills in ZKP security. Plus, find out how you can contribute to expanding this invaluable resource!

Stefanos Chaliasos, Chenyang Yu · August 09, 2024

Verifying Poseidon in Clean: Why the Last 'sorry' Is About Primality

We walk through a Lean 4 proof of correctness for a Clean model of circomlib's optimized Poseidon hash circuit at arity 1. The theorem says the modeled constraints are sound and complete with respect to the optimized Poseidon spec. After weeks of work, the only remaining `sorry` was a primality proof for the BN254 scalar field: a 254-bit number that no proof assistant can decide by trial division. Closing it requires a Pratt certificate, a recursive proof structure based on a theorem Lucas published in 1876.

Martin Ochoa · May 04, 2026

Proofs On A Leash: Post-Quantum Lattice SNARK With Greyhound

In this engaging blog post, we dive into the future of cryptography by exploring how lattice-based proof systems could fend off the quantum threat. We break down Greyhound, a promising lattice-based solution, explaining its transparent nature, efficient construction, and adaptability with today's systems. Along the way, you'll get a glimpse of key concepts like lattices, Ajtai commitments, and how Greyhound cleverly ensures security and efficiency. Whether you’re curious about the cutting-edge of cryptographic research or just want to understand the basics of quantum-resistant solutions, this post offers both depth and clarity.

David Wong · June 03, 2025