No need to take the AI's word for it: Claude delivers a mathematical proof for software

AI writes an ever larger share of all software, and increasingly also the checks on it. That raises a difficult question: how do you know it is right, if nobody can read all the work any more? On 22 October 2026 Anthropic showed an answer. The AI delivers not only the work, but also a proof that the work does what it should do, and a small, trustworthy program checks that proof. You then do not have to take the AI's word for it.

Anthropic did this together with Theorem, a company that checks software mathematically. They had the AI model Claude examine 123 widely used open-source libraries: free building blocks that are in countless apps, websites and servers, for example to compress files or show images. Claude proved that they do not crash, and along the way found hundreds of bugs that had stayed hidden for years.

A proof instead of a promise

If you ask an AI assistant today to check code, you get an answer like "I have checked it, it is fine". Whether that is true, you have to find out yourself. Here it works differently. Claude writes a complete mathematical worked solution showing why the code works for every input, just as a pupil writes down every step in a maths test.

Those worked solutions are enormous: a typical proof has about 600,000 lines. No human reads that. Nor is there any need to, because a small checking program, Rocq, recalculates every step, like a teacher who marks a worked solution line by line. If one step is wrong, the whole proof is rejected. Anyone who wants to trust the result therefore only has to trust that checking program, plus the exact agreement on what had to be proved. This is called formal verification.

Rocq is not AI itself. The French research institute Inria started work on it in 1984, and the first version appeared in 1989, then still under the name Coq. Mathematicians and computer scientists have relied on it for decades. In 2002, for example, it was used to check the proof of the famous four colour theorem: every map can be coloured with four colours without neighbouring countries getting the same colour.

This approach also works for code that Claude writes itself. When Claude found a bug, it fixed it and then proved that the new version does work correctly. To prevent cheating, for example turning a program into something that no longer does anything and therefore never crashes, repairs were given penalty points and the team checked them afterwards. In a separate test Claude wrote a program itself that can run a large part of the programming language Python, and proved that it behaves like the official version.

Ordinary tests miss a lot

Software is normally tested by bombarding it with random input, like a child pressing all the buttons at once. Google does this day and night for many open-source projects. But a test only sees what goes wrong with the input that happened to be tried. A proof covers all input, in this case every file up to 64 megabytes.

The difference showed at once. According to Anthropic, Claude found hundreds of bugs in a few weeks that had gone unnoticed for years despite trillions of test runs. Many of them are memory errors, where a program writes or reads outside its own piece of memory. Attackers can sometimes use such errors to take over a computer. A few examples:

• A program that unpacks compressed files only went wrong with a file of about 20 megabytes with one rare structure.
• A program that reads images only failed with a file of 64 megabytes and more than 2 gigabytes of working memory. Tests rarely make them that large.
• A function that should limit which files an app may open did not always do so. Nothing crashed, so no test noticed it.
• Claude independently rediscovered a known security hole in libexpat, a widely used building block that reads XML files. That hole was closed this year.

In a program that reads PDF files, the team found as many security bugs in one week as are normally reported in a whole year. Another important program contained a logic error that had gone unnoticed for more than ten years.

What the proof does and does not say

Mathematically proven does not mean free of errors, the researchers themselves stress. The proof applies exactly to what was agreed: the program does not crash. An error where nothing crashes falls outside it.

The proofs also apply to a simplified situation: programs that do one task at a time, on processors of the RISC-V type, an open design that anyone may use. Most laptops and phones use a different type. The next steps are those common processors and programs that carry out several tasks at the same time.

And it is still expensive: one proof can cost hundreds of millions of tokens, the small pieces of text a language model works in. That is falling fast. In one test Claude Opus 5.5 needed about 40 per cent less computing than the previous model, Opus 5.

Anthropic and Theorem are putting part of the proofs online publicly, so that others can check them themselves. Proofs that would give away security holes that have not yet been closed are being held back for now. Theorem offers open-source projects to have their code checked in the same way.

What does this mean for the road to the singularity?

The faster AI works, the bigger the problem of checking its work becomes. People cannot read everything an AI makes in a few weeks, and that limits how much work we dare to leave to AI. A proof that a machine can check removes that brake: trust then no longer lies in the AI itself, but in a small program that anyone can check.

Work that used to take years of human effort per project, Claude did here for 123 libraries together in a few weeks. If proofs become cheaper and also start to apply to ordinary computers, AI will be able to build important software and show that it is sound. That is a solid foundation for a world in which AI does more and more of the work.

What is the technological singularity? Read the explanation →