saved
Auditing in the age of (good enough) AI
Hraness wrote this summary from a saved copy of the source. Quotations are taken word for word from the source.
gist
Fredrik Dahlgren of Trail of Bits describes six months of agent-built tooling before a Miden zkVM audit: an LSP, decompiler, static analyses, and a Lean model of the executor. The work found an unvalidated prover advice input that could forge Falcon signatures, plus 95 machine-checked core-library proofs, arguing agents changed the economics of exploratory audit prep.
ideas
- Prep tooling beats starting at agentic code review. Agents now make custom LSP, decompilation, analysis, and formal models worth building before the engagement starts.
- MASM had almost no tooling. Stack-machine Miden assembly made implicit dataflow hard to review, so the team spent lead time on language support.
- Static analysis caught a high-severity bug. An underconstrained remainder in mod_12289 let a malicious prover forge Falcon signatures and drain Falcon-keyed accounts.
- Lean proofs cover when bugs are absent. Ninety-five correctness proofs over binary arithmetic also found two unit-test misses in rotr and wrapping_mul.
- Failed side projects now cost tokens. Agents made exploratory prep viable without selling clients on uncertain tooling work in advance.
quotes
“before code review even starts, agents now allow us to build custom tooling and formal models that improve the quality and depth of our reviews.”
“A malicious prover could exploit this to forge Falcon signatures and drain any Miden account controlled by a Falcon key pair.”
“Today, a failed side project only costs tokens.”