ZK/SEC Quarterly

formal-verification · auditing

Checking the Checkers and Auditing the Ironwood FV

Cryptographic software is error-prone and failures are catastrophic, therefore formal verification is a powerful and increasingly practical tool for greatly improving the assurances of our cryptographic software. But who verifies the formal verification? Formal verification itself is software too, what is proved, under which assumptions and its relation to the real-world implementation lie beyond the scope of the machine-checked proof. In this post, we want to give some insights into our three-week audit of the Ironwood formalization and some of the common pitfalls that formal verification more broadly can encounter.

Mathias Hall-Andersen October 05, 2026 8 min Read →

Proof is in the Pudding · Part 11

Archetype x zkSecurity - Proof is in the Pudding: zkML

In Session 11 of "Proof is in the Pudding," we look at what it takes to prove model inference. We cover transformer computation, sumcheck, GKR, lookup arguments, quantization, and KV caching, then discuss scaling and possible uses for verifiable ML.

ZK/SEC September 30, 2026 1 min

announcement · clean

Intro to Clean for Devs.

We think that Clean is the future of circuit development, so we created a programmer-first introduction to show circuit developers who have never used formal verification how they can build circuits faster, safer and better.

Mathias Hall-Andersen September 29, 2026 1 min

Variants of KZG 3 of 5 parts in this issue

Part 5

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

Part 4

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

Part 3

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

security · audit

Fiat-Shamir Bugs: How One Missing Line Breaks a Proof System

This blog post looks at Fiat-Shamir from a practical security perspective: it explains why something that seems simple in theory can become surprisingly easy to get wrong. By using vulnerabilities found in real-world projects, we give developers and reviewers a better way to think about Fiat-Shamir when designing, implementing, and auditing proof systems.

Giap Vu, David Wong September 19, 2026 28 min

AI · formal-verification

Better Codes - and how they can be worse if you're not careful

An exploration of how an AI tried to work around a security feature to handle a theorem that was hard to prove.

Kobi Gurkan September 14, 2026

security · AI

The Year Finding and Exploiting Bugs Became Cheap, and What to Do About It

The economics of security have changed. AI has made finding and exploiting bugs cheaper, including in cryptographic and zero-knowledge code, while validation and remediation remain slow. Here is our view of what happened, what comes next, and how teams should change the way they secure their stack to defend against AI-assisted attackers.

Stefanos Chaliasos September 07, 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

zkvmBlast · Part 1

Introducing zkvmBlast: Differential Fuzzing for Ethereum's zkVMs

zkVMs are moving to the center of Ethereum's roadmap, which means a bug in a zkVM is turning into a bug in Ethereum itself. We built zkvmBlast, a zkVM-agnostic differential fuzzer that runs the same program across SP1, RISC0, OpenVM, Pico, Zisk, and Airbender against a reference simulator and flags any disagreement. It hunts for both soundness and completeness bugs, with a deliberate focus on completeness, an under-explored class that can turn a single valid block into a liveness failure. We share the first batch of findings.

Stefanos Chaliasos, Martín Ochoa, Varun Thakore August 10, 2026

security · AI

Circom-Auditor: Open-Source Skills for Finding Vulnerabilities in Circom Code

We are releasing zk-skills, a set of open-source security skills for AI coding agents, starting with circom-auditor: a first line of defense against vulnerabilities in Circom circuits, compatible with both Claude Code and Codex. On the zkbugs benchmark it detects up to 66 of 70 known bugs when pointed at the vulnerable circuits, and up to 40 of 56 when let loose on the full original codebases, far ahead of existing Circom security tools.

Stefanos Chaliasos, Hao Pham August 05, 2026