March–April 2026

Audit of the Stwo-Cairo Verifier

StarkWare

Review of StarkWare’s Stwo-Cairo verifier, the Circle STARK verifier for Cairo programs, covering its FRI low-degree test, the Cairo AIR, LogUp lookups over the M31 field, and the Fiat-Shamir transcript.

Audit of Mina's Decentralised Treasury

Mina

Review of Mina’s decentralized treasury, built with o1js, covering its Poseidon hashing and Merkle tree commitments.

Audit of Aptos Encrypted Mempool

Aptos

Review of Aptos’s encrypted mempool, which uses threshold identity-based encryption to keep transactions hidden until they are ordered. The audit covered the distributed key generation, the BLS and KZG components, and the sigma-protocol proofs with their Fiat-Shamir transcripts.

Soundness Failures in LaBRADOR Implementations from NTT-Friendly Rings

We reviewed several LaBRADOR implementations on GitHub and found three of them broken, with soundness collapsing as far as a single bit. The cause is parameter choices that look reasonable for lattice protocols, a power-of-2 modulus, a composite modulus, or NTT-friendly rings, and the post explains how each one undermines the soundness argument.

The Final Form of Software Development

A case for writing assembly directly alongside Lean proofs, with AI agents producing both, which sidesteps the problem of trusting a compiler. It walks through real EVM 256-bit addition code next to its specification to show what the approach looks like in practice.

Sum-Check as an Algebraic Tensor Reduction: Part I

The first post in a series that frames recursive proof protocols as algebraic tensor reductions, using sum-check as the running example. It walks through one recursive step, the prover’s univariate summary, the verifier’s consistency check, and the reduction to a smaller claim, with a small bivariate example.

Archetype x zkSecurity - Proof is in the Pudding: ZK on Bitcoin

Session 09 looks at verifying zero-knowledge proofs on Bitcoin. It covers Bitcoin’s UTXO model and Script limits, then MPC-based approaches and BitVM’s optimistic verification with fraud proofs, including timelocks, Lamport signatures for state, Taproot, simulated covenants, BitVM 3 with garbled circuits, cut-and-choose, and witness encryption.

Cryptography challenges @KalmarCTF 2026

Minsun gives a high-level tour of the hard cryptography challenges he wrote for KalmarCTF 2026, the ideas behind their design, and how subtle randomness failures and algebraic structure can turn into deep vulnerabilities.

KZG vs IPA vs FRI: Picking the Right Polynomial Commitment Scheme

A practical guide to the trade-offs between KZG, IPA/Halo, and FRI, the three main polynomial commitment scheme families behind modern proof systems. It compares proof sizes, verification costs, trust assumptions, benchmarks, and on-chain gas costs.

zkbugs

The open ZK vulnerability dataset was rebuilt. Each circom bug now ships with its full codebase and compiles in two modes, the original and the patched version, so tools can be run against real before-and-after code. The collection grew past 100 bugs, drawing on public audits from Veridise, OpenZeppelin, and others, and gained an automated pipeline for ingesting new findings.

clean

The Verified-zkEVM Lean4 library extended its soundness proofs to VM-style channel ensembles, with a Fibonacci VM as the worked example, and its FemtoCairo pipeline now handles memory-reading instructions. It also added a Poseidon hash circuit with soundness and completeness proofs, a generic IsEqual gadget for any provable type, and a FiniteField typeclass covering prime and binary fields. The prover and verifier environments were split so soundness proofs no longer see the prover’s hints.

zkHydra

zkHydra can now run against the whole zkbugs dataset in analyze, evaluate, or both modes, parallelized across jobs, with a triage helper for working through findings. zkbugs is no longer bundled as a submodule, so users clone it themselves.