Timeline
Direct answerDated milestones in formal verification of zero-knowledge circuits and cryptographic implementations: framework releases, completed proofs, bugs found by verification, and bugs that escaped it.
- 2026-09-09Nethermind archives Horus, its SMT verifier for Cairo 0
Lean-based verification of the Cairo AIR by StarkWare is now the only maintained route for Cairo. - 2026-08-20Ethereum Foundation, Yukon and zkSecurity launch better.codes
An open autoresearch challenge to raise the Lean-checked soundness bound of the koalaIRS12 proximity problem; by 2026-09-13 the bound rose from 64 to 68.07 bits. - 2026-08-01zkSecurity releases zk-skills with circom-auditor
Open-source security skills for coding agents, reporting 66 of 70 known bugs found on the zkbugs benchmark. - 2026-07-23StarkWare verifies the STRK20 privacy pool in Lean 4
More than 230 theorems using the Cairo AIR methodology. - 2026-07-02zkSecurity launches zk.golf
Circuit optimisation challenges where every submission carries a kernel-checked Lean proof of soundness and completeness. - 2026-06-05Clean adds Channels for multi-table and zkVM verification
Presented at ZKProof 8; lifts per-table soundness to whole-system soundness for LogUp-style interactions. - 2026-06-03StarkWare and Avigad publish Lean 4 soundness of the S-two Cairo AIR
Satisfying the AIR implies a correct Cairo execution, for both Stone and S-two. - 2026-05-28Rust-to-Lean pipeline verifies Plonky3 FRI folding and RISC Zero Merkle checks
hax, Aeneas, ArkLib, CompPoly and AI provers combined on production prover code. - 2026-05-20Ethereum Foundation discloses SP1 Hypercube JALR bug and audits sp1-lean
51 of 62 opcodes fully proven; the JALR theorem's alignment assumption is the public case study in specification gaps. - 2026-05-04zkSecurity proves circomlib's Poseidon sound and complete in Clean
BN254 primality discharged via a Pratt certificate in CompPoly. - 2026-05-01Apple publishes formal verification of corecrypto ML-KEM and ML-DSA
Isabelle/HOL with AutoCorres2, plus SAW and Cryptol, over C and ARM64. - 2026-04-08Veridise releases LLZK v1.0
Circom and Halo2 frontends; Picus, zkLean and R1CS backends; Rocq via Formal Land. - 2026-02-15Verification Theatre paper reports 13 bugs in verified libcrux and hpke-rs
Four inside verified ML-KEM and ML-DSA code, all outside what the specifications stated. - 2025-12-18Ethereum Foundation publishes the L1 zkEVM security roadmap
100-bit provable security by May 2026, 128-bit and a formal soundness argument for recursion by end of 2026. - 2025-11-19zkSecurity publishes a hands-on comparison of six circuit FV frameworks
ACL2, acl2-jolt, Garden, zk-lean, sp1-lean and Clean evaluated on reproducibility and practical proving. - 2025-10-09Nethermind and Succinct announce Lean verification of SP1 Hypercube core chips
RV64 chip constraints proved against the Sail RISC-V model, built on Clean. - 2025-07-02Nethermind's Halva finds a critical bug in Scroll's deprecated Keccak Halo2 circuit
The clearest public case of a proof-assistant framework finding a critical circuit bug. - 2025-03-27zkSecurity introduces Clean
A Lean 4 DSL for ZK circuits with soundness and completeness proofs per gadget.