Prevent,Contain,Prove

In brief

For decades, the cost of expert labor set a practical limit on software attack. Finding an important vulnerability took weeks or months of specialist work; turning it into a reliable exploit took more. Frontier AI is removing that limit. Attack capabilities that once required a nation-state are becoming available to criminal groups and individuals, and the interval between discovery and exploitation is shrinking.

The answer is not to patch faster. This report argues for changing how consequential software is built, isolated, evaluated, and procured, using a family of high-assurance techniques that exist today and have already survived contact with production. The largest software companies run formal methods programs at scale; verified cryptographic code ships inside mainstream browsers and operating systems; and in DARPA's HACMS program, red-teamers given a foothold inside a military drone could not break out of its mathematically verified isolation boundaries.

For decision makers, these techniques serve three functions, which together define the strategy:

• PreventMake important defect classes impossible by construction.
• ContainLimit what a successful compromise can accomplish.
• ProveEstablish critical properties through rigorous, machine-checkable analysis.

High-assurance engineering is a spectrum, not a cliff. At one end are practices any competent engineering organization can adopt today: memory-safe languages, rigorous static analysis, coarse-grained compartmentalization. At the other are machine-checked proofs of correctness for the most critical components. The report lays out a phased adoption arc through baseline, intermediate, and advanced stages, and asks organizations to state explicit assurance claims and back them with inspectable artifacts: evidence, not checklists.

Cities did not fight fires by hiring more firefighters alone; they wrote building codes — requiring fire-resistant materials, mandating firewalls between units, and inspecting the result — and applied them first and most strictly to the buildings where failure would cost the most.

AI cuts both ways. The same models that accelerate vulnerability discovery are making specification and proof cheaper, and trust derives from the checker and the reviewed specification, not from the author of the evidence, human or AI. Where high-assurance engineering has been adopted, the economic returns have been consistently positive. What remains is to build the tools, workforce, institutions, and demand signals while defenders can still act deliberately rather than in response to catastrophe.