Formal verification in ZK and cryptography: timeline of releases, proofs and findings (2025-2026)
================================================================================

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-09: Nethermind 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. (https://github.com/NethermindEth/horus-checker)
2026-08-20: Ethereum 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. (https://blog.ethereum.org/en/2026/08/20/better-codes-challenge)
2026-08-01: zkSecurity releases zk-skills with circom-auditor — Open-source security skills for coding agents, reporting 66 of 70 known bugs found on the zkbugs benchmark. (https://blog.zksecurity.xyz/posts/circom-auditor/)
2026-07-23: StarkWare verifies the STRK20 privacy pool in Lean 4 — More than 230 theorems using the Cairo AIR methodology. (https://starkware.co/blog/strk20-formal-verification/)
2026-07-02: zkSecurity launches zk.golf — Circuit optimisation challenges where every submission carries a kernel-checked Lean proof of soundness and completeness. (https://blog.zksecurity.xyz/posts/zkgolf/)
2026-06-05: Clean adds Channels for multi-table and zkVM verification — Presented at ZKProof 8; lifts per-table soundness to whole-system soundness for LogUp-style interactions. (https://blog.zksecurity.xyz/posts/clean-verified-zkvms/)
2026-06-03: StarkWare 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. (https://arxiv.org/abs/2606.04311)
2026-05-28: Rust-to-Lean pipeline verifies Plonky3 FRI folding and RISC Zero Merkle checks — hax, Aeneas, ArkLib, CompPoly and AI provers combined on production prover code. (https://arxiv.org/abs/2605.30106)
2026-05-20: Ethereum 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. (https://zkevm.ethereum.foundation/blog/sp1-fv)
2026-05-04: zkSecurity proves circomlib's Poseidon sound and complete in Clean — BN254 primality discharged via a Pratt certificate in CompPoly. (https://blog.zksecurity.xyz/posts/poseidon-clean/)
2026-05-01: Apple publishes formal verification of corecrypto ML-KEM and ML-DSA — Isabelle/HOL with AutoCorres2, plus SAW and Cryptol, over C and ARM64. (https://github.com/apple/corecrypto)
2026-04-08: Veridise releases LLZK v1.0 — Circom and Halo2 frontends; Picus, zkLean and R1CS backends; Rocq via Formal Land. (https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/)
2026-02-15: Verification 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. (https://eprint.iacr.org/2026/192)
2025-12-18: Ethereum 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. (https://blog.ethereum.org/2025/12/18/zkevm-security-foundations)
2025-11-19: zkSecurity 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. (https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/)
2025-10-09: Nethermind and Succinct announce Lean verification of SP1 Hypercube core chips — RV64 chip constraints proved against the Sail RISC-V model, built on Clean. (https://blog.succinct.xyz/nethermind-lean/)
2025-07-02: Nethermind'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. (https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean)
2025-03-27: zkSecurity introduces Clean — A Lean 4 DSL for ZK circuits with soundness and completeness proofs per gadget. (https://blog.zksecurity.xyz/posts/clean/)

Source page: https://sorryfree.com/news/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13