Why we verify AI-generated code instead of scanning it

An AI coding assistant now writes the first draft of most code that reaches a pull request. It writes fast, it writes plausibly, and it writes at a volume no human review process was designed to absorb. The security question is no longer "did a person introduce a bug." It is "can anything keep up with a machine that produces code faster than anyone can read it."

The reflex answer is to point a scanner at the output. Run the static analyzer, run the linter, run the rules. That reflex is where things quietly go wrong, and it is worth being precise about why.

The trapWhat a scanner actually does

A scanner works by recognition. It carries a library of known-bad shapes, taint rules keyed to specific functions, patterns for specific frameworks, a list of sanitizers it trusts, and it asks of every line: does this match something I already know? That model has a structural ceiling. It can only catch what someone thought to enumerate, and it can only reason about libraries someone thought to encode.

AI-generated code breaks that model from both ends. The AI reaches for framework A this week and framework B next week. It writes a one-line helper that behaves like a sanitizer but appears in no list. It composes a data flow across four files that no single pattern spans. Every gap in the enumeration is a gap the scanner cannot see, and the enumeration is never finished, because the domain it is trying to cover is unbounded.

The inversionThe AI declares. Acutis verifies.

Here is the move. The hard part of program analysis, the part that keeps a scanner enumerating forever, is semantic inference: figuring out what an unfamiliar function means. Is it a source of user input? A sink that reaches a database? A transform that escapes HTML? A scanner has to guess, and it guesses from a list.

But there is already a system in the loop that knows exactly what each function means, because it just wrote it. The AI. So we invert the responsibility. The AI declares the security semantics of its own code as a contract: these are the sources, these are the sinks, these are the transforms. Acutis does not infer any of it. It takes the contract and verifies that the declared properties actually hold across every data flow.

# the AI declares; Acutis does not guess
contract = {
  "sources": ["request.args.get"],        # user-controlled
  "sinks":   [{ name: "cursor.execute",
               category: "SQLQuery" }],    # a boundary
  "transforms": [{ name: "parameterize",
               effect: "ParameterizesSQL" }]  # a defense
}

This turns the analyzer's hardest problem into the AI's easiest one. The verifier carries no function lists, no pattern library, no trusted-sanitizer set, no framework knowledge at all. It is name-blind. A framework it has never seen works on day one, because it never needed to know the framework, only the contract.

The coreA lattice, not a checklist

Underneath the contract is a small formal object. Every value carries a set of security properties, and those sets form a lattice. At the top sits everything dangerous. At the bottom sits the empty set, which is safe. A parameter from the outside world enters at the top. A literal enters at the bottom. Concatenation takes the join of its parts. A declared transform can move a value down the lattice, but only if Acutis can confirm the transform really does what the contract claims.

Verification is then a single, decidable question asked at each sink: has the value flowing in reached the bottom for that boundary? SQL output must not carry SQL metacharacters. HTML output must not carry HTML metacharacters. If it has not, the flow is unsafe, and Acutis can hand back the exact path that proves it.

The outputThree verdicts, no score

Acutis does not return a risk number for a human to triage. It returns a typed judgment.

In practice it runs as a loop inside the assistant, before the code ever reaches you. The AI proposes code, Acutis blocks with a path, the AI rewrites, Acutis allows. The security-blocked pull request goes to zero, because the block happened upstream and the false positive never reached a person.

The stanceZero trust, and why over-blocking is the safe direction

When Acutis meets a call the contract did not describe, it does not shrug and assume the value is fine. Unknown goes to the top of the lattice, and the top is dangerous, so the verdict is a block. That is deliberate. The failure mode of a verifier should be caution, not silence. A false block costs the AI one more rewrite. A false allow costs you a vulnerability in production. We would rather be told to say more than be allowed to say nothing.

ScopeWhat this does not claim

A verifier that overstates itself is just a scanner with better marketing. So, plainly:

Within those lines, the engine has been measured. On 136 SQL-injection and cross-site-scripting cases from CVEFixes, with oracle contracts, it scored an F1 of 1.0: no false positives, no false negatives. In an end-to-end study with an AI agent across 40 paired prompts, the vulnerability rate fell by a 62.5 percentage-point absolute reduction, from 62.5% to 0%, with zero regressions and a McNemar p-value of 5.96 × 10^-8. We publish the caveats in the same breath as the numbers, on purpose. The full method is in F1 = 1.0, and 62.5 points to zero.

The bet is simple, and it is the whole company in one sentence. Stop trying to enumerate everything that could go wrong. Ask the system that wrote the code to say what it meant, and prove it.