Building software that comes with a proof
Traditional testing looks for errors: run a system through enough scenarios and hope you find the failures before someone else does.
Formal methods take a different approach – proving the absence of entire classes of errors, by using rigorous mathematical techniques to prove that software or hardware behaves as specified across all permitted inputs and states.
This distinction matters more and more, as AI makes it possible to generate code, models and decisions much faster than people can realistically inspect them. We are increasingly relying on systems too complex, and consequential, to secure through testing alone.
Recent cyber incidents are a reminder of what is at stake. Earlier this month, ASOS said that it was investigating unauthorised activity after attackers used its app to send customers a threatening push notification, and that some personal information may have been accessed. Last week, the discovery of two critical PHP flaws prompted governments and companies around the world to take websites offline while they install emergency patches. The vulnerabilities could allow unauthenticated attackers to run code on unpatched servers, and exploitation attempts have already been reported.
Formal methods would not by themselves prevent every kind of breach, like social engineering or stolen credentials. But they could help us build a stronger foundation for the future: critical components that do exactly what they are designed to do, with mathematical proof as evidence that can be checked rather than simply trusted.
An eight week marathon
Our Safeguarded AI programme is exploring whether AI-enabled formal methods can make that level of assurance practical at the scale modern digital infrastructure demands.
We are backing eight new research projects with £22m to test whether AI can help produce proofs for production-grade software and hardware. The challenge is to do this quickly and affordably enough for high-assurance cyber defence to be used far more widely, rather than only in a small number of specialist systems.
The Blue Teams will build the systems and the proof that they work as intended. An independent central Red Team will try to find weaknesses in those claims.
The projects range from systems for containing AI agents to protecting code running on millions of Android devices: places where a demonstrably correct component could create resilience far beyond a single company or application.
The teams began on 1 September and are working in eight-week sprints, each ending with the Red Team stress-testing what they’ve built and proved. Each cycle is an opportunity for us to learn about what AI can accelerate, where human expertise remains indispensable, and whether formal methods can provide the guarantees needed for critical digital infrastructure.
Meet the Creators
The first projects in the programme take different routes towards the same question: can formal methods and AI help us build digital systems that are secure by design, and prove it?
Project AIVHAI — Capabilities Limited, with lowRISC, Sigil Logic, Cherified Systems + Google Research
AI is moving out of the data centre and into the things around us, from AR headsets to biometric door locks and factory robots. On these devices, AI models typically share one chip, and nothing in today’s hardware reliably keeps them apart, meaning that a compromised model can reach data it shouldn’t. This team is extending CHERI, a hardware security architecture that checks every memory access against what each piece of software is allowed to touch, to cover the chip’s AI processing units. The result seals models off from each other and from the rest of the system, with mathematical proof that this holds right down to the circuit design.
AI-Scale Protocol Verification in LLVM/MLIR — University of Cambridge, with Bristol, INESC-ID + Utah
Most of the software you use was translated by a compiler before it ran, and a bug in the compiler can quietly become a bug in everything it builds. LLVM is the compiler infrastructure behind much of the world’s software, and like every widely used compiler it carries no mathematical proof that it works correctly: it changes daily, and proofs have never kept up. This team is proving that the security guarantees of WireGuard, a widely used VPN, survive compilation. They are building a formal twin of LLVM in Lean, a language for machine-checked proofs, and showing it preserves the properties WireGuard depends on — with AI constructing and repairing those proofs as both pieces of software evolve.
Agentic-seL4 — University of Sheffield, University of Surrey + the University of Melbourne
AI agents are being handed the keys to real systems: files, tools, networks. They are kept in check by sandboxes, which are ordinary unverified software, and agents have already escaped them during lab tests, in some cases breaching another company’s production infrastructure. This team is building an agent sandbox on seL4, the core of an operating system that comes with mathematical proof that programs can only touch what they have been explicitly granted. seL4’s strongest guarantees assume permissions are fixed when the system starts. The team is extending these guarantees to permissions that change while an agent runs, making it possible to prove that the sandbox enforces dynamic policies. For example, a policy might say that once an agent has read a confidential file, it can no longer send anything over the network.
Verifiable Browse-Down — PentenAmio, Kry10 + Galois
Someone working on a sensitive or isolated network who needs to look something up online can’t simply open a browser, because one malicious webpage could compromise the whole network. The standard solution runs the browser on separate hardware and passes only a video of the screen across. But it needs dedicated equipment, sometimes a full rack, so it is mostly confined to fixed installations in the highest-risk organisations. This team is fitting it onto a single chip, running Kry10’s operating system built on seL4. That makes it small enough for mobile and portable use as well as fixed sites. Two new high-level properties, proven on top of the existing seL4 proofs, take over the job that separate hardware used to do. First, every browsing session is wiped completely when it ends, leaving an attacker nowhere to persist. Second, no video stream, however malicious, can break the software that displays it on the sensitive side.
Keystone — Imperial College London + EPFL
Every prompt sent to an AI service passes through layers of software that receive it, run it through the model and return a response, usually for many users on the same machines at once. As we come to increasingly use AI across our social and economic lives, this inference stack is becoming critical infrastructure in its own right. Because it sees every conversation and holds the model itself, flaws in it can expose users’ data, silently corrupt answers that millions of people rely on or leak the model itself. The team is testing whether they can build a high-performance inference stack that comes with formal proofs which eliminate these vulnerabilities. They start with the code that does a model’s arithmetic on graphics chips and work up the stack layer by layer, towards AI infrastructure citizens, governments and businesses can trust.
Verified pKVM — Rigorous Engineering
On millions of Android phones, a small piece of software called pKVM has been developed by Google to let some of the most sensitive work, such as on-device AI, be walled-off from the rest of the phone. A flaw in pKVM would be shared by every one of those phones. This team aims to prove mathematically that (under stated assumptions) pKVM is bug-free, cannot be corrupted, and prevents information leaks — so that even an attacker who has taken over the rest of the phone’s software cannot get through to what it protects. Proofs like this usually require rewriting the software from scratch. This team is proving the code that already ships, so the result applies to software already running on phones, and demonstrates how formal verification can work on production real-world systems software.
CNI Guardian - Kry10
The pumps, valves and switches of power, gas and water networks are often run by decades-old controllers that speak protocols designed before cyberattacks were a concern, and safety certification makes it hard to patch or update them. At best they are protected by commercial firewalls, which have vulnerabilities of their own. This team is building a network guard that checks every message to and from this equipment against a precise specification of what is allowed, with mathematical proof that every message it lets through complies with the protocol. AI helps turn long, ambiguous protocol standards into formal, human-validated specifications, from which the gateway code is generated automatically along with its proof. The guard itself runs on a formally verified operating system kernel, making the device far harder to attack. It will be tested against real control equipment and known attacks.
Trail of Bits — Central Red Team
A formal proof is only as strong as the assumptions behind it. Trail of Bits is the programme’s independent Red Team: testing whether the Blue Teams’ security claims hold up under pressure.
That means looking beyond the code itself — for gaps in specifications, weaknesses in verification tools, a mismatched threat model, or assumptions that do not stand up in practice. Their role is not simply to find failures, but to sharpen each team’s end-to-end assurance case and help them build software people can genuinely rely on.
Early results show what could be possible
The teams are only at the beginning, but the initial results are starting to test the programme’s central bet: that increasing AI capabilities could move formal methods from a specialist practice into a tool that can scale to protect our most critical infrastructure.
The strongest early signal is about speed. Work that would once have taken months of specialist time is now, in some cases, being done in days, with AI systems taking on substantial portions of engineering and proof work under human oversight. If results like these hold, formal guarantees could move from an exception to a realistic expectation for critical software. The question shifts from ‘is this possible?’ to ‘is it practicable at scale?’
The results also suggest that this is not speed alone. Teams are building formal models of complex, deployed systems and testing verified components against conventional implementations. Those comparisons are an essential first step towards trustworthy deployment: a proof is useful only if its model captures the behaviour and security property that matter in practice.
An important shared frontier is specification. AI can search for proofs quickly, but defining the right security property, rather than merely reproducing the existing implementation, still demands extensive expert judgement, testing and adversarial scrutiny. As projects progress, teams will also push into a new set of practical questions, such as finding scalable ways to keep proofs current as the underlying systems continue to evolve.
Follow along by signing up for the Trust Everything, Everywhere mailing list for future sprint updates and results.
