A Lean4 formalization of the paper "A Simplified Round-by-round Soundness Proof of FRI" by Albert Garreta, Nicolas Mohnblatt, and Benedikt Wagner, completed using Harmonic's Aristotle agent and Claude Code. Welcome to the strange world of machine-led formalization of cryptography.
In Session 08 of "Proof is in the Pudding," we explore how different networks have approached privacy over the years. From E-Cash and Monero to MobileCoin and Zether, we break down blind signatures, Pedersen commitments, stealth addresses, ring signatures, and more. This session provides a comprehensive tour of the techniques used to break linkability, hide addresses, and obscure transaction data in the name of privacy and safety.
Think you have what it takes to join zkSecurity? We're raising the bar with a second challenge! Now candidates must complete both zkBank and our new Curve Machine challenge to prove their skills across the full spectrum of ZK security. Are you ready to take on both challenges?
A new interactive tutorial on Sumcheck, Multilinear Extensions, and HyperPlonk with complete SageMath implementations and exercises. Go beyond the theory and understand how these protocols actually work by implementing them yourself.
In this blog post, we explore how to optimize the sumcheck protocol, particularly when working with values in a small field and randomness from a large field, as often needed in zkVMs. We introduce various algorithms aimed at reducing expensive operations, focusing on minimizing large multiplications. Starting from using simple evaluation tables to more sophisticated techniques like precomputing accumulators and leveraging Lagrange interpolation, we demonstrate how to efficiently organize computations to speed up proving times. Readers will gain insights into handling arithmetic operations within the sumcheck protocol and learn about optimizing specific cases in zero-knowledge proofs.
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.
Learn the fundamentals of Σ-protocols through the classic Schnorr protocol, exploring the three-step dance of commit, challenge, and respond. This post walks through knowledge soundness and witness extraction, then shows how to compose Sigma proofs with AND/OR logic and Pedersen commitments. See working SageMath implementations, discover how Fiat-Shamir transforms interactive proofs into non-interactive signatures, and understand the deeper mathematical structure as proofs of knowledge of homomorphism pre-images.
In this final part of our series on Circle STARKs, we tie together concepts from Mersenne prime fields, circle curves and bivariate polynomials to showcase a comprehensive Circle STARK protocol. We detail the process of arithmetization over the circle curve, introducing Circle FRI as a low-degree test and walk through the complete Circle STARK construction. Readers will explore how trace commitments, constraint batching and low-degree proofs combine for efficient verifiable computation, delving into the nuances of proof validity and security analysis.
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.
In this post, we explore LaBRADOR, a transparent, lattice-based proof system that achieves sublinear proof sizes through recursion. Built on the Module-SIS assumption, LaBRADOR lets a prover efficiently demonstrate knowledge of short vectors satisfying dot product constraints, general enough to express R1CS. The protocol’s key ideas include amortized openings, outer commitments, and a strategy to shrink the witness after each round of recursion. Together, these techniques make LaBRADOR a powerful, scalable framework for post-quantum zero-knowledge proofs.
This article breaks down how Bulletproofs enable range proofs: proofs that a hidden value lies within a range without revealing it. Starting from bit decomposition, it shows how to express and combine constraints into a single inner product, then make the proof zero-knowledge with blinding polynomials and commitments. By the end, you’ll understand how systems like Monero’s confidential transactions prove valid amounts while keeping values private.
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.
