A software flaw that survives testing can interrupt deliveries or expose customer information. Anthropic and Theorem now report using AI to find bugs, repair the code and produce mathematical proofs that specified errors cannot occur in the repaired version, under defined conditions.
For Norwegian companies, the opportunity is better protection before software enters service. A supplier can provide evidence for a particular repair instead of relying only on tests that happened to pass. The important limit is that a proof covers a precise claim about particular code. It does not establish that the whole service is secure.
This article explains what the researchers achieved, how a mathematical proof differs from a test, and what management should ask before buying software supported by such evidence.
What did the researchers do?
In research published on 22 October 2026, Anthropic describes work with Theorem in which Claude found bugs while trying to prove security properties. Claude repaired the affected code and continued until it could produce proofs for the chosen requirements.
The company reports proofs for 239 test entry points across 123 open-source libraries, reusable collections of code used by other programs. An entry point is where a test tool feeds data into the code. These figures do not mean that 123 complete libraries were proved free of bugs.
The result matters because the work goes beyond finding another problem for a developer to investigate. It connects discovery, repair and a checkable argument that the repaired code meets a specified rule. These are the developers' reported results, not an independent measurement of benefits in Norwegian businesses.
How is a proof different from a test?
A test runs the program with selected examples. If a file reader handles those files correctly, the test passes. A different file could still reveal a defect that the examples missed.
A formal proof takes a precisely defined rule, such as the absence of specified crashes, and establishes that it holds for every input within the stated limits. It depends on a mathematical description of the program and its environment being accurate. This method is called formal verification.
AI writes the mathematical argument. A separate proof checker checks whether it establishes the chosen rule. That is different from asking the same chatbot to declare its own code safe. Specialists still need to assess whether the rule and assumptions describe what matters in the actual service.
A useful proof therefore answers a narrow question thoroughly. It does not answer every question about the software.
What has not been proved?
The public proof repository listed 60 entry points in 25 libraries when checked on 26 October. This is a released subset of the larger experiment. The documentation describes proofs about specific executable files and errors detected by the included checking tools. It does not establish the correctness of whole libraries or rule out a program running forever. The proofs were not independently rerun for this article.
That distinction has a business consequence. A conversion service that never crashes but never finishes still fails its customer. Avoiding a specified crash, returning the right result and finishing on time are separate requirements.
The reported experiment used fixed executable files built for RISC-V, a processor design, and a mathematical model of Linux. The proofs depend on that setup and on limits for input data and memory. A company using different files or operating conditions cannot assume that the proofs apply unchanged.
Such assumptions are a normal part of formal verification. The established seL4 project documents its own assumptions, including hardware behaviour and system startup. That separate work does not validate Anthropic's results. It illustrates why the conditions belong alongside the claim.
Follow one customer file through the service
Consider a hypothetical Norwegian manufacturer receiving drawing files from customers. A supplier converts the files into a format employees use to prepare quotations. A defect in the file reader interrupts conversion and holds up the work.
Suppose the supplier offers a proof that a particular reading function cannot produce a specified error. The manufacturer's technical adviser should first check whether it covers the file types, sizes, software version and operating environment the company actually uses.
Then examine the rest of the service. It must receive the file, keep it accessible only to the right customer and authorised staff, convert it and return a usable result. A proof about the reader does not automatically cover those other steps. It also cannot establish that the drawing contains the right dimensions for the order.
The proof may still remove an important failure mode. Management's task is to understand that improvement and ensure that other controls address the remaining risks. A limited guarantee can be valuable without becoming a guarantee of the entire business.
Ask the supplier five plain questions
Before relying on the proof, ask for a short explanation alongside the technical documentation:
- Which error has been ruled out? Ask what remains possible, including incorrect results or a job that does not finish.
- Which version does it cover? Identify the executable file and its digital fingerprint so the technical team can compare it with the version in service.
- Under which conditions? Check input limits, dependencies and operating assumptions against the company's actual setup.
- How was the proof checked? Obtain the material and a practical way to check it, or agree a qualified independent review. A generated assurance paragraph is insufficient.
- What happens after an update? Name who checks the new version and removes any assurance claim that no longer has support.
These questions are a proposed purchasing aid, not a certification scheme or a universal legal requirement. A small AS can use a qualified supplier or external adviser for the technical assessment. Management needs an understandable explanation of the protection it is buying, not the ability to read mathematical proof code.
Test whether the method is worth buying
Start with one important component that handles external files or data and a requirement that can be stated precisely. Commission a limited feasibility assessment before committing to a large programme. Count specialist review, engineering and maintenance of the proof alongside AI costs.
Compare the work with other ways to reduce the same risk: removing an unnecessary file type, isolating conversion from critical systems, replacing an unsuitable component or improving existing tests. Choose the option that addresses the company's exposure and resources.
Do not dismiss the method solely because it used to demand too much specialist effort. A bounded investigation can establish whether stronger assurance is now practical while existing protections remain in place. It may also show that another measure offers better value.
Management owns the assessment, supplier follow-up and release decision. For material risks or investments, the board should ask what business failure the work prevents, what remains unresolved and how the assurance will stay current. Directors should not select proof tools or approve individual code changes.
Use the guide to customer cybersecurity evidence when assessing a supplier's security promises. The article on response before a patch exists covers failures that still require rapid action. Better prevention and faster response are both necessary.
The practical question is: Which important error has the supplier proved impossible in the version we will actually run? The answer determines how much weight the company should give the proof.
Sources checked on 26 October 2026. The manufacturer and proposed purchasing questions are hypothetical. Recommendations are the author's analysis. The reported research does not prove all software secure. The AI-generated illustration represents the boundary of a mathematical claim, not an actual research proof.