zkDaily - 2026-09-22

零知识证明zkDaily

ZKP Frontier Tracker 🎯

Tue

09.22

2026

Auditing in the age of (good enough) AI

Blog

https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/

MidenzkVMLean

Trail of Bits shared how AI agents audited the Miden zkVM by building an LSP, decompiler, static analysis engine, and Lean models, uncovering a critical Falcon signature forgery bug and validation flaws.

NotesNotes要点

Built an LSP server, decompiler, and static analysis engine for MASM from scratch
Critical bug: unvalidated prover-supplied advice values enabled Falcon signature forgery and fund theft
Static analysis identified 400+ type validation improvements reachable from the public API
Produced 95 machine-checked Lean correctness proofs covering core library binary arithmetic
AI-assisted discovery of two subtle bugs in rotr and wrapping_mul missed by unit tests
Demonstrates the economic viability of AI agents for high-assurance security audit tooling

Collected by @icerdesign

零知识证明zkDaily

Q&A Deep Dive 💬

Tue

09.22

2026

How did AI assist the Miden audit?

AI agents built an LSP, decompiler, static analysis engine, and Lean models to uncover critical bugs and verify correctness.

What components did Lean proofs cover?

They covered 95 correctness proofs for all binary arithmetic components in the core library, ensuring expected stack semantics.

Why is MASM decompilation hard to guarantee?

MASM lacks declared signatures and a calling convention, while loops and branches have variable stack effects, causing static inference to fail.

Prompted by @icerdesign