Everyone Says 'Verified.' Ask What You Get.

Every tool in the AI code quality market now says it verifies your code. Review bots verify. Test generators verify. Fuzzers and simulators verify. Proof engines verify. We verify.

When everyone uses the same word, the word stops carrying information. If you are deciding what to put between AI-generated code and production, you need a sharper question. Here is the one I use:

What artifact do I get, and what fraction of the inputs does it cover?

Not the category, not the demo, not the dashboard. The thing you are holding after the tool runs - the thing you could hand to a teammate, an auditor, or yourself at 2 a.m. during an incident.

Then ask the harder follow-up: what about that artifact will convince the people you show it to that they should trust it?

That question has two parts.

Is the artifact credible on its own? Can someone check it without taking your word, or the tool's word, for anything? A counterexample can be replayed by anyone with a Python interpreter. A proof can be re-checked by an independent checker. A paragraph of review comments can only be read and believed - or not.

Is the source of the artifact credible? How was it produced, and how does that process fail? A deterministic checker has known, stated failure modes: it can time out, it can be out of scope, it can be checking against the wrong reference. A model's judgment fails in ways nobody - including the vendor - can fully reconstruct after the fact. An artifact that has to borrow its credibility from the tool's reputation is weaker than one that carries its own.

Six things "verified" can mean

What the tool does	The artifact you get	Inputs covered	Why a skeptic would believe it
AI code review	Comments: a model's opinion that the change looks right or wrong	Whatever the reviewer happened to reason about	Only if they already trust the reviewer. The opinion cannot be independently re-checked.
Generated tests	A test suite, and the diff in its results	The inputs the tests exercise	They can re-run it. But tests generated from today's code lock in today's behavior - bugs included.
Simulation and fuzzing	A list of failures found, or none, within a bounded search	The states reached within the time and depth budget	Each failure can be reproduced. "None found" is not "none exist."
Runtime and agent checks	Logs of checks that passed while the code ran	The executions that actually happened	The logs show what did happen, not what could.
Proof against a specification	A machine-checked proof that the code meets a written spec	All inputs, relative to the spec	The proof can be re-checked independently. They still have to believe the spec is right and complete.
Equivalence proof	A proof that new code behaves identically to a reference version - or a concrete counterexample	All inputs, relative to the reference	The proof can be re-checked and the counterexample replayed. They still have to believe the reference is right.

Every row is useful. They are not interchangeable.

The two columns that matter

The artifact column separates things you have to take on trust from things you can check. An opinion and a log describe what a tool concluded. A proof or a counterexample can be checked by someone who does not trust the tool at all - which is exactly the person you need to convince when something goes wrong, or when a regulator asks how you know.

The coverage column separates sampling from exhaustiveness. Tests and fuzzing are good at what they do; they find real bugs quickly and cheaply. But they answer "did we see a problem?" A proof answers "can there be one?" The hardest bugs live at the boundaries - the century year, the zero modulus, the negative length - and boundaries are where sampled inputs are thinnest. (For a worked example, see the calendar problem.)

Every row has a catch, including ours

Proofs are not magic. Every proof is relative to something.

A proof against a specification is only as good as the specification, and writing a complete spec is the work that has kept formal methods out of most engineering teams for decades.

An equivalence proof is only as good as the reference. If the original function had a bug, proving the new one equivalent proves it has the same bug. We say this plainly in our own documentation, because it is the first thing a careful engineer will ask.

And no proof tool reaches every function today. I/O, concurrency, and some language features are still hard. A tool that says "inconclusive" when it does not know is more useful than one that guesses - and a tool that reports a confidence level should tell you what that number is backed by. That is part of the source's credibility too: a tool that states its own limits is easier to believe about everything else.

So add one more question: what is the result relative to, and what is out of scope?

Why this got urgent

AI made writing code nearly free. It did not make reviewing it any cheaper. The volume of changes is going up; human attention is not.

When a model writes a change and another model reviews it, you have two opinions. They may well be good opinions. But a probabilistic judge of probabilistic code is still a judgment, and judgment does not compose into evidence just because there is more of it.

The fix is not to stop using models. It is to separate who proposes from who decides. A model can propose a change; something whose reasoning can be checked should decide whether it ships. The credibility of the result then comes from the checker, not the proposer.

That is why we built FMToolkit around the last row of the table. Most teams do not have specifications. They do have a version of the code that works. That version is the reference, and every change - human or AI - can be checked against it, producing either a proof or the exact input where behavior diverged. (We have written up what happens when you put that check behind an LLM.)

Six questions to ask any vendor - including us

1. What artifact do I get? An opinion, a log, a test diff, a proof, a counterexample?
2. Can someone who doesn't trust your tool check it? Or does it only make sense if they already believe you?
3. How was it produced, and how does that process fail? Are the failure modes known and stated?
4. What fraction of inputs does it cover? All of them, a sample, or only the ones that happened to run?
5. What is it relative to? A spec, a reference implementation, a model's judgment?
6. What does it do when it doesn't know?

The answers don't pick a single winner. They tell you how to layer: review for intent and readability, tests for the behaviors you care about, fuzzing for the surprises, and proof wherever a silent behavior change costs more than the check.

Ship what's proven, not assumed.

FMToolkit is a GitHub App, and the launch plan is free. Install it and try it on your next pull request.