All issues

zkSecurity Newsletter

January–February 2026

In this issue: zkao launches in early access, the first real-world ZK exploits get dissected, and a Lean4 proof of FRI soundness.

February 28, 2026

Welcome to the first issue of the zkSecurity Newsletter, a note every two months on what we have been auditing, researching, and building.

We launched zkao in early access, our AI security platform for zero-knowledge circuits, and wrote up the thinking behind it in “Security That Compounds.” zkao starts with Circom support and two analysis flows, SnarkSentinel and Invariants Hunter, and picked up Gnark circuits, public reports, and proof-of-concept triage in its first weeks.

On the research side, the first two real-world exploits against live ZK circuits happened, and both came from Groth16 verifiers with a botched trusted setup rather than subtle under-constrained bugs. We also published a Lean4 formalization of FRI’s round-by-round soundness, covered Google’s use of Gemini to find a bug in a SNARGs-from-LWE paper, looked at one-round finality in BFT consensus, and ran the eighth “Proof is in the Pudding” session on privacy in payment networks.

We are also catching up on recent public reports: reviews of INTMAX’s zERC20, an Aleo multisig wallet, and three engagements for Lighter and Hyperlane. In open source, the Verified-zkEVM clean library can now export a Lean-defined circuit to JSON and prove it end to end on Plonky3, and zkHydra picked up a command-line interface, Docker images, and support for the zkbugs dataset.

Highlights

In this issue

AI

zkao is live

We launched zkao in early access, our AI security platform for zero-knowledge circuits. It starts with Circom and two analysis flows, SnarkSentinel and Invariants Hunter. Read the launch →

Research

The first real-world ZK exploits

Two live ZK circuits were exploited in the same week, both from Groth16 verifiers with a botched trusted setup rather than the under-constrained bugs the field expected. Read the analysis →

Research

A machine-checked proof of FRI soundness

We formalized the round-by-round soundness of FRI in Lean4, following the paper by Garreta, Mohnblatt, and Wagner, using Harmonic’s Aristotle agent together with Claude Code. Read it →

Audits

Five recent public reports

New reviews span private transfers, Aleo wallets and integrations, and Lighter’s rollup exchange, including INTMAX’s zERC20 and an Aleo multisig wallet.

Audits

Public audit reports

Research

From the blog & research

  • The First ZK Exploits Happened, and They Weren't What We Expected

    The first two known exploits against live ZK circuits both trace to the same root cause: Groth16 verifiers generated by snarkjs with an incorrect trusted setup that skipped the last step. These were not subtle under-constrained bugs. One was rescued by white-hat hackers for about $1.5M, the other was drained for 5 ETH.

  • When LLM Review Cryptography Papers

    Google Research used Gemini to find a bug in a cryptography paper on SNARGs from LWE. We walk through how the events unfolded, the iterative self-correction prompting they used, and the growing role of LLMs in academic research.

  • Optimistic One-Vote-Round Finality in BFT Consensus

    An intuition-first walkthrough of why 33% BFT needs two voting rounds, how 20% designs reach true one-round finality, and how an optimistic fast path bridges the gap.

  • zkao: Security That Compounds

    The thinking behind zkao: making AI security research work the way fuzzing does, not as a one-shot event but as something you run continuously until coverage compounds.

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

    A Lean4 formalization of the paper by Albert Garreta, Nicolas Mohnblatt, and Benedikt Wagner, completed with Harmonic’s Aristotle agent and Claude Code. A look into machine-led formalization of cryptography.

  • Archetype x zkSecurity - Proof is in the Pudding: Privacy in Payment Networks

    Session 08 walks through how different networks have approached privacy over the years, from E-Cash and Monero to MobileCoin and Zether. It breaks down blind signatures, Pedersen commitments, stealth addresses, and ring signatures, and the techniques used to break linkability and hide transaction data.

Tooling

Releases & open source

  • zkao 0.1.0

    zkao launched in early access: AI-powered security analysis for Circom circuits, with two flows (SnarkSentinel for deep audits and Invariants Hunter for targeted bug hunting) and GitHub scanning. Two follow-up releases the same month added Gnark circuit support, public shareable reports, and proof-of-concept generation in Circom triage.

  • clean

    The Verified-zkEVM Lean4 library added a channel-based interaction model for lookup and multiset arguments and proved its comparison gadgets sound and complete. Its Plonky3 backend gained a generic lookup framework with multi-column lookups and prover-provided tables, on top of Plonky3’s built-in LogUp and batch STARK. A Lean-defined circuit can now be exported to JSON and proved end to end, shown with a FemtoCairo example.

  • zkHydra

    zkHydra gained a command-line interface with separate analyze and evaluate modes, Docker images with automated publishing, and support for running against the zkbugs dataset. A new –vanilla mode runs the underlying tools without zkHydra’s extra orchestration.

Get the next issue in your inbox

One email every two months. Audits, research, and tooling from the zkSecurity team.

No spam. Unsubscribe anytime.