May–June 2026

Audit of Zeko's circuits, sequencer and DA layer

Zeko

Review of Zeko, a Mina layer-2, covering its Pickles and Kimchi recursive proof circuits, the sequencer, the data availability layer, and the threshold signatures and Merkle trees behind them.

SnarkVM ECDSA and Serialization Instructions

Aleo

Review of new SnarkVM instructions for Aleo, covering ECDSA verification over secp256k1, Schnorr signatures, and the Keccak and SHA-3 serialization paths.

Audit of Aptos Confidential Assets

Aptos Labs

Review of Aptos’s confidential assets, which use twisted ElGamal encryption with Bulletproofs and sigma-protocol proofs over ristretto255 to keep balances and transfers private on Move.

Aleo Dynamic Dispatch

Aleo

Review of Aleo’s dynamic dispatch mechanism, covering its Poseidon hashing, Schnorr signatures, and Merkle tree commitments.

Clean: From Verified Circuits to Verified zkVMs

Clean, our circuit DSL, is growing toward verifying complex multi-AIR ensembles. The post introduces channels as a way to model lookups, permutation arguments, and zkVM cross-table interactions, then shows how local gadget proofs compose into global soundness theorems. It comes with our talk from ZKProof 8.

zkNews Is Now Open to Everyone

zkNews is now open to everyone. Access was limited to a small beta at launch to keep things stable, and that rate limit is gone. Anyone can sign up, submit links, and join the discussion at news.zksecurity.xyz.

Breaking Jolt's Verifier with an Unbound Uni-Skip Claim

We found a critical soundness bug in Jolt’s transparent verifier that let a forged proof for an invalid execution pass. It was fixed quickly after disclosure, and the full proof-of-concept and write-up are in the linked repository.

Announcing mpcsec.org: What Goes Wrong When You Implement MPC

mpcsec.org is a new collaborative reference for common pitfalls in MPC implementations and the primitives they rely on, built with contributors from zkSecurity, Trail of Bits, Partisia, and Zama. It is a starting point for anyone who builds, audits, or deploys threshold signatures, distributed key generation, or other MPC protocols.

Powers-of-Funbenius

A one-character repeated-squaring bug in Inferno’s Limbo implementation turns the intended random polynomial check into a linearized Frobenius check over a binary extension field. The post explains why the usual Schwartz-Zippel argument disappears, how the periodicity of the Frobenius map makes collisions immediate after 64 multiplication gates, and how smaller circuits can cheat with even higher probability.

Groth16, Intuitively

A ground-up build of Groth16, the SNARK behind 128-byte proofs and constant-size verification. It starts from R1CS and QAPs, then layers in pairings, the trusted-setup parameters, and the alpha, beta, gamma, delta separator tricks that make the scheme sound, so every term in the verifier equation has a reason.

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

A Lean 4 proof that a Clean model of circomlib’s optimized arity-1 Poseidon circuit is sound and complete against the Poseidon spec. After weeks of work, the last remaining sorry was a primality proof for the 254-bit BN254 scalar field, which no proof assistant can decide by trial division. Closing it took a Pratt certificate, a recursive structure based on a theorem Lucas published in 1876.

Encrypted Mempools: Security Beyond Encryption

Encrypted mempools are an emerging way to reduce transaction-ordering MEV. They add a new security boundary around the exact moment a transaction becomes plaintext, which ordinary mempools do not have. The post lays out the security model, the core invariant, and the failure modes designers need to watch for.

Notes and Proofs for Divisor Techniques

Self-contained notes and proofs for Eagen’s divisor-based ECIP protocol, written with Diego F. Aranha and supported by MAGIC Grants. They work through the algebraic geometry, the interactive proof and its soundness, the composition with a simulation-extractable NIZK, and the R1CS verifier circuit used by Parker’s gadget in Monero’s FCMP++.

Sum-Check as an Algebraic Tensor Reduction: Part II

The second part of the series introduces the algebraic language for framing sum-check as a tensor reduction, starting with rings and modules. Rings generalize fields by dropping the requirement that every nonzero element has an inverse, and modules generalize vector spaces by letting scalars come from a ring. The post uses plenty of examples to build intuition.

Sum-Check as an Algebraic Tensor Reduction: Part III

The third part is about the maps that move between modules without breaking their structure: when a map is linear, when two modules are secretly the same, and why two-input maps deserve special attention. By the end it has the tooling needed to tackle abstract tensor products.

On ZK Security, ZK Summit, and a Decade of Progress

Ahead of sponsoring zkSummit14 in Rome on May 7th, a look back at a decade of progress in zero-knowledge, the current state of ZK security drawn from more than 100 audits, and why events like zkSummit have become infrastructure for the field.

Do Fees in Rollups Bring Attacks?

Honest Majority by Common Prefix

Stefanos Chaliasos joins the Honest Majority podcast to explain how mispriced fees in major rollups open up practical attacks: DA saturation, which floods data availability and delays finality, and prover killers, which exploit instructions that are cheap to run but expensive to prove.

Clean: From Verified Circuits to Verified zkVMs

ZKProof 8, Rome

Our ZKProof 8 talk in Rome on growing the clean Lean framework from single circuits to whole zkVMs. It introduces channels to model lookups, permutation arguments, and cross-table interactions, so local gadget proofs compose into global soundness.

zkao 1.0

zkao went public with version 1.0, generally available with access still reviewed per team, with sharper analysis flows and runnable proof-of-concept exploits. Before that, 0.4.0 and 0.5.0 moved scans to a credits budget, added Aleo/Leo and Plonky3 coverage, and introduced the gestalt analysis flow on Opus 4.8, reaching beyond ZK circuits into broader cryptography. After 1.0, 1.1.0 ordered findings by impact and ran scans in parallel, and 1.2.0 added regression checks on fixed findings and manual control over severity.

zkHydra 0.1.1

zkHydra added a new analyzer, ConsCS, to its set of integrated tools, and cut a tagged 0.1.1 release that publishes multi-arch Docker images on version tags.

clean

The Verified-zkEVM Lean4 library added a SHA-256 circuit with soundness proofs for its compression gadgets and merged the verified circomlib Poseidon circuit. A new auto-elaboration tactic removes manual boilerplate from circuit definitions, and the core is now free of sorry placeholders, with every circuit interaction-aware.