Securing software quality when AI writes the code:which proof protects which rule?

A case that comes up regularly in software development: hundreds of test files, and only a handful of checks that use the product the way a person uses it. Some of the tests check whether a little label has the right color. It shows during a refactor that changes nothing for anyone, and still dozens of tests go red. The other way round, too: things that are genuinely broken, and everything stays green.

So what does a green check actually tell you? Three terms help.

A unit test checks a single small component on its own. Like checking whether one brick can take the load.

Code coverage says how much of the code ran during testing. It doesn’t say whether anyone looked at what came out. 87 percent means 87 percent of the lines were touched once.

And then there’s the mock. To make a test fast, you swap the database, the payment service or the mail program for a stand-in that always answers politely.

Say you rehearse your loan meeting with your brother-in-law playing the bank. He says yes, and you go home relieved. The real bank has different forms, and that is exactly how a test against a mock works. It proves your code gets along with your idea of the database. Only the real database shows whether the idea is right. I call this mock theater: test and code share the same wrong assumption, and both play their parts perfectly. So the first thing to secure is that the mock has the same interface as the real system: it understands the same questions and answers in the same shape. That’s your contractor’s job, not yours. But it helps to understand what quality even means here.

Every brick tested. The house never entered.

A research team led by Asma Hamidi recreated exactly this workflow. Five language models write code and the tests for it. More than 6,000 faulty programs in total. The result, in their words: actual fault detection rates remain extremely low, often near zero (Source: Hamidi et al., 2026). The tests run through the broken spot, but they don’t ask the right question there. To be fair: it’s a preprint, and the same paper says simple bugs get caught well. The hard ones are the problem.

A second paper from the University of Toronto looked at more than 100,000 AI-written test cases from eleven models. Once you can’t be sure the code under test is correct, coverage stops being a reliable sign of whether bugs get found (Source: Zhao, Zhou and Cohen, 2026). This belongs here too: if the code is considered correct and the tests only guard future changes, coverage does work as a signal. Coverage is a diagnostic. It isn’t a verdict on quality.

Maren’s report was true. It just answered a question she never asked.

The other yardstick is surprisingly unspectacular: it fits on one sheet.

You know your business. You know what must never happen. That’s enough to start.

Three questions find your rules. What would embarrass you in front of a customer? What costs money immediately if it goes wrong? What must never end up with the wrong person?

For Maren, these are the five sentences:

1. A statement never goes to the wrong household.
2. An invoice never goes out twice.
3. What’s saved is still there after a restart.
4. Blocked beats approved. If an account is blocked, nothing goes out, no matter which other permissions are set.
5. No payout over 500 euros without a second approval.

No jargon in there. Anyone in the office can tell whether the sentence is true.

Each sentence becomes a chain: rule, proof, the layer it sits on, and the workflow where the rule shows up in daily life. The old question was: how many tests are there? And how high is coverage? The new one is the proof question: which proof protects this rule? The first question always has an impressive number for an answer. The second gets either an answer or an honest silence.

Practitioners know the idea as risk-based testing. What’s new is who can ask it: as long as tests were expensive, their number was a decent sign of care, and the question stayed with the developers. Now that tests cost next to nothing, it belongs to the person who knows the rules. To you.

Martin Kleppmann of the University of Cambridge put his finger on why the rule part stays with people. Once checking becomes automatic, the difficulty moves to writing the requirement down correctly: how do you know that the properties that were proved are actually the properties you cared about (Source: Kleppmann, 2025)? No machine can take that off your hands. And that’s good news. Your knowledge of your business becomes more valuable as code gets cheaper.

In my view, the rules matter more than the function they happen to be coded in. Code gets rebuilt. The rule stays.

A test is a sample. You try ten cases and hope the eleventh works too. A proof is a calculation that holds for all cases at once, the way you don’t have to try every number to know that even plus even is even. The technical term is formal verification.

Why has this been out of reach for small and mid-sized businesses so far? The most famous example, a proven operating-system kernel, had 8,700 lines of code. The proof took 20 person-years (Source: Kleppmann, 2025). That was 2009.

Now something is shifting. In December 2025, Martin Kleppmann predicted that AI will bring this method out of its niche and into everyday software engineering (Source: Kleppmann, 2025). Then again, predictions are hard, especially about the future (after a Danish saying often attributed to Niels Bohr; Source: Quote Investigator, 2013). Amazon says it already uses such proofs in several products and writes that as AI agents move money and approve claims, the standard approach to testing is no longer sufficient (Source: Amazon Science, 2026). That comes from a company investing in the technique itself.

The damper comes from a benchmark at ICML 2026. Ask current models to write proven code for classic algorithms and, depending on the proof language, they succeed in 40.3, in 24.7 or in only 7.8 percent of cases (Source: Zhao et al., ICML 2026). An older comparison from September 2025, with different tasks, came out at 82, 44 and 27 percent (Source: Beneficial AI Foundation and MIT, 2025). My reading: it works, the success rate swings widely with task and proof language, and it’s a long way from “one click for the whole product”.

Where the limit lies shows in a case from April 2026. Kiran Gopinathan took a file-compression program that had been proven correct and hit it with about 105 million random inputs. In the proven part: zero memory errors (Source: Gopinathan, 2026). Still, he found two bugs, and both sat outside what the proof covers (Source: Gopinathan, 2026). One was in a part nobody had written a rule for. The other was in the foundation the proof trusts blindly. His conclusion: verification is only as strong as the questions you think to ask and the foundations you choose to trust.

A pattern follows that practitioners will recognize. Write the rule down once, small and exact, and prove it. Then run the real code against that small version with a very large number of random inputs and see whether both always give the same answer. In one Amazon project, the proven model is about ten times smaller than the production code (Source: Lean FRO, undated). In an older write-up from 2024, the proofs there found 4 bugs, and checking the model against the code found 21 more (Source: Disselkoen et al., 2024).

Donald Knuth put this limit into one sentence back in 1977, at the end of a note on an algorithm: “Beware of bugs in the above code; I have only proved it correct, not tried it.” (Source: Knuth, 1977). The rule is proven. Whether the code follows it is something you check on top.

Which rule is a good fit? It’s unambiguous: same input, same result. It rarely changes. A failure would be expensive. It fits on one page and works without a user interface and without a network. For Maren, that’s “Blocked beats approved” and “No payout over 500 euros without a second approval”. The rest stays with journeys and boundary tests.

You tidy up one corner at a time. Here’s yours: 60 minutes, one sheet, five sentences. Take it to the person or the agent building your software and ask the proof question about each sentence. Then follow up with a second one: show me that it turns red when the rule breaks.

You can hear four answers.

• “There’s a journey test against the real system for that.” Good.
• “That’s in the unit tests.” Ask: against the real database or against a mock?
• “We test that manually before the release.” Honest, but not a proof that goes red on its own.
• Silence. Also an answer. Now you know where to start.

A look ahead, without legal advice. For products with digital elements, reporting obligations under the European Cyber Resilience Act have applied since 11 September 2026, and the main obligations apply from 11 December 2027. The regulation requires technical documentation of the means the manufacturer uses to ensure the requirements are met (Source: Regulation (EU) 2024/2847). And the new EU Product Liability Directive explicitly counts software as a product and applies to products placed on the market from December 2026 (Source: Directive (EU) 2024/2853). Whether your project falls under this is a question for legal advice, not for me. The direction is clear, though: the question of how you prove your software does what it should will be asked more often. If you can answer it with five sentences and five proofs, you have a solid start.

Writing the rules down is human work. Proving them is machine work. When the two are cleanly separated, you no longer have to click through the program yourself every evening to sleep well. Your head is free for what only you can do: the conversation with the customer, the decision about what gets built next.

Every important rule deserves a proof, right where a failure would hurt. With small teams, I build exactly that bridge: from five sentences in the office to proofs in the product that turn red the moment a rule breaks. If your proof question was met with silence, that’s where my work begins.

Take a sheet today and write down the first sentence. The one that just made you a little uneasy.

All names of individuals and companies used in this article are fictitious. Any resemblance to real persons or businesses is purely coincidental and unintentional. The examples are provided solely for illustrative purposes.