Security auditing in the age of (good enough) AI | AI Paper Digest

TL;DR Highlight

Six months of agent-built tooling found a high-severity bug and produced 95 Lean proofs.

Who Should Read

A developer who wants to use agents for code review or security audits beyond simple bug hunting.

Core Mechanics

Agents built the tools before the review
- Before auditing Miden VM, Trail of Bits spent six months having agents build an LSP server, decompiler, static analysis engine, and Lean model from scratch.
- The target used a custom assembly language (MASM) with almost no developer tooling.
The decompiler's real value was its IR
- The decompiler took over 100 AI-generated commits.
- Its analysis framework and intermediate representation (IR) turned out most useful and were reused for static analysis.
Claude built, Codex reviewed
- After each feature, agents decompiled random procedures and compared them with the original.
- Issues found became regression tests for the model to fix.
Static analysis found a high-severity bug
- It flagged over 400 locations with weak type validation plus one high-severity issue.
- In mod_12289 the prover-supplied remainder was never validated, letting a malicious prover forge Falcon signatures.

Community Reactions

An opinion that 'good enough' AI for auditing is like good enough brakes
- Security leaves no room for complacency.
An opinion that you should assume you will eventually be breached and redesign your architecture
- The commenter says security firms need a new way to do business.
A view that this shows AI used to do things better, not just faster
- Building tooling and formal proofs is seen as a positive example.

How to Apply

Have an agent build a small CLI for an unfamiliar codebase
- Ask Claude Code for a script that extracts symbols and call relations from the repo you review today.
- Require a verification step comparing output with the source.
Split the builder and reviewer agents
- Use one model to implement and another to review.
- Turn each issue found into a regression test.
Build a pass that checks input validation
- Write an analysis that checks external values get type and range validation, and add it to CI.
- Start with spots reachable from the public API.
Try formal proofs on core pure functions
- Start with small side-effect-free functions and have the agent write correctness theorems in Lean.
- The tool checks proofs, so humans only read the theorem statements.

Try It

copy & run

# Paste into Claude Code: simplified version of the paper's method (input validation audit)

You are a security reviewer. Find every point in {{directory}} where external input enters (request params, values from external services).

For each point, tabulate (1) type validation (2) range validation (3) any path that uses the value before validation.

Then for each suspected gap, write a reproducible test and run it to confirm it actually fails.

Next to try: have another model review the results to filter false positives.

Terminology

LSP (Language Server Protocol)A standard that gives editors features like autocomplete and go-to-definition. Think of it as a USB port for language features.

Stack machineAn architecture where instructions pop values from a stack and push results back. Inputs are implicit, so code is hard to read.

Advice valueA precomputed input the prover supplies through a separate stack. The verifier must validate it, like checking a handed-in answer sheet.

Abstract interpretationAnalysis that tracks value types like '32-bit integer' or 'unknown' instead of real values, looping until nothing new appears. A passing check holds for every run.

LeanA proof assistant that machine-checks mathematical theorems. It's like a type checker that fails to compile if the proof is wrong.

Related Papers

Related Resources

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