Proof, Not Promises: Trusting Code Written by AI

AI is great at writing code and building tools. More and more, it’s writing the tools AI agents use to read files, process data and take actions on our behalf.

So how do you know that code is safe?

Today, we mostly rely on two things: alignment and sandboxing. But alignment is probabilistic, and sandboxing a full operating system is coarse and leaves a large attack surface. Meanwhile, the real safety bottleneck is human code review, and it can’t keep up with how fast AI writes code.

There’s another option: proof.

AI has also gotten surprisingly good at mathematical reasoning and formal proofs. So why not have AI write machine-checkable proofs about the code it writes? Humans only need to review the specification and a small verifier, not every line of code.

In this webinar, we will share what he’s learned, and why he thinks this is where trustworthy software is headed: AI writes the code, AI writes the proof, and humans decide what “correct” and “safe” actually mean.

We’ll cover:

• Why alignment and sandboxing alone don’t tell you what AI-written code will actually do
• The kinds of evidence available, from an adversarial review by another AI to a formal proof, and why high assurance may finally be worth the cost
• Why “what did you prove?” is the question that matters: functional correctness, confinement and information flow are very different guarantees
• How information flow labels can keep sensitive data from leaking, for example letting a research agent use the internet while blocking it from sensitive data
• Why a verified component is only as trustworthy as your ability to stop an unverified one from impersonating it, and where hardware attestation and certificates come in

We’ll also walk through our experiments with proof-carrying agent tools, and what they could mean for how organizations decide which code, and which agents, to trust.