September–October 2026

Midnight Circuits and Proof System Follow-up Audit

Midnight

Our third audit for Midnight, covering changes to the PLONK proof system in midnight-zk, including the trash argument and committed instances, and its trusted setup.

Audit of Midnight Halo2 Fork

Midnight

Review of Midnight’s Halo2 framework, a fork of PSE Halo2, covering its changes to the PLONK proof system and lookups.

Audit of Midnight Foreign Field, ECC & Hashing Circuits

Midnight

Review of the Halo2 circuits for the Midnight network: foreign-field arithmetic, elliptic curves, hash-to-curve, Poseidon, SHA-256, and Merkle trees.

Audit of Midnight Circuits (2)

Midnight

Review of additional circuits from Midnight’s standard library, written in Halo2.

Adversarial Testing of the Ironwood Formal Verification

Zcash

Instead of a conventional code review, we injected knowledge-soundness bugs into the Rust implementation and the Lean model of Zcash’s Orchard circuit and Halo2 stack, then checked whether Ironwood’s formalization rejected them.

End-to-End Audit of SecondFi's recovery flow

SecondFi

Review of SecondFi’s recovery flow, where users recover funds by proving in zero knowledge that a master key derives a compromised key. It covered the verifiers, the soundness and completeness of the flow, and the web security of the recovery app.

Audit of OpenVM 2.0

Axiom

A four-phase audit of OpenVM 2.0, covering the SWIRL proof system, the native and recursive STARK verifiers, the continuations aggregation pipeline, and the new deferral framework.

Audit of SecondFi's proof-tool circuits and prover patches to gnark

SecondFi

Review of the gnark circuits and prover patches that let users prove ownership of a Cardano wallet credential in the browser without revealing private keys or derivation paths. Two high-severity issues in the upstream code were found and fixed.

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.

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.

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.

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.

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.

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.

Zero Knowledge Episode 414: zkGolf, AI, Clean and Optimising ZK Circuits

Zero Knowledge Podcast

Mathias and Giorgio join Anna Rose and fellow zkSecurity teammates Nico and Kobi on the Zero Knowledge podcast to talk about Clean, zkGolf, and what happens when AI agents compete to build better circuits with proofs of correctness.

zkao 3.0

zkao 3.0 adds organizations, which put projects under one team with shared roles and one credit balance, and our biggest analysis update since launch: three new techniques, scans that build on earlier analysis, and coverage for trusted execution environments and Noir. Scan types are now named for the job (Quick Look, Deep Audit, Continuous Testing, Dependency Watch), and a new assistant briefs you and answers questions about your scans.

zk.golf

Four new challenges: BLS12-381 G1 scalar multiplication in variable- and fixed-base versions, the Keccak-p[800, 12] permutation over GF(2), and extracting claims from a Google ID token, the first parsing challenge.

clean

The Verified-zkEVM Lean4 library got a website at clean.zksecurity.xyz and moved to Lean’s module system. A new compiler emits WebAssembly text and exports R1CS constraints for snarkjs, and the Plonky3 backend gained AIR witness generation, fixed columns, and memory support.