eighteen entries
Timeline
Direct answer
Dated 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 0Lean-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.codesAn 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-auditorOpen-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 4More than 230 theorems using the Cairo AIR methodology.
- 2026-07-02zkSecurity launches zk.golfCircuit 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 verificationPresented 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 AIRSatisfying 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 checkshax, Aeneas, ArkLib, CompPoly and AI provers combined on production prover code.
- 2026-05-20Ethereum Foundation discloses SP1 Hypercube JALR bug and audits sp1-lean51 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 CleanBN254 primality discharged via a Pratt certificate in CompPoly.
- 2026-05-01Apple publishes formal verification of corecrypto ML-KEM and ML-DSAIsabelle/HOL with AutoCorres2, plus SAW and Cryptol, over C and ARM64.
- 2026-04-08Veridise releases LLZK v1.0Circom 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-rsFour inside verified ML-KEM and ML-DSA code, all outside what the specifications stated.
- 2025-12-18Ethereum Foundation publishes the L1 zkEVM security roadmap100-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 frameworksACL2, 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 chipsRV64 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 circuitThe clearest public case of a proof-assistant framework finding a critical circuit bug.
- 2025-03-27zkSecurity introduces CleanA Lean 4 DSL for ZK circuits with soundness and completeness proofs per gadget.