I appreciate Theodore Ehrenborg's comments.

As a wee lad, I heard about mathematical certainty of computer programs. Let’s go over what I currently believe and don’t believe.

First: what is formal verification

Sometimes you get pwned because of the spec-implementation gap. The computer did not do what it should’ve done. Other times, you get pwned by the world-spec gap. The computer wasn’t wrong, your “shoulds” were.

Expanding the domain of compiletime knowledge

A compiler tells you the problem with your code when it is, in some sense, “wrong”. When you can define the sense in which your code can be “wrong”, you have circumscribed some domain of compiletime knowledge. In other words, you’ve characterized the kinds of things you can know at compiletime.

The less you know at compiletime, the more you find out at runtime. The less you can afford to wait till runtime to find out, the more you need to know at compiletime. This is, I claim, a fundamental tradeoff. You like to know as much as you can at compiletime; when you know very little at compiletime, the job that you expect to take a week crashes on day five.

Isolating the bug surface to the world-spec gap, or sidechannels

When we have a proof, we know that an implementation matches the specification exactly and that it won’t be attacked by cramming some assumption violation between the implementation and specification. It may be attacked via the world-spec problem, but not the spec-implementation problem^[1].

Side channels are why we, in the movement for AI Security via Formal Methods, will repeatedly but counterintuitively say that formal verification is a source of swiss cheese, i.e. another layer in a defense-in-depth strategy. Previously, position papers have caused problems by taking the opposite stance^[2].

Exploiting inductive structure

Why does reality let us get away with this? In some sense, the more correct question is why do syntax and semantics let us get away with this, since spec-implementation relationships are in the realm of symbols (computers aren’t literally in the realm of symbols, since our abstractions only start after the physical realm takes a back seat). In any case, the answer is because we can exploit inductive structure. In the natural number case, we can know something for sure about an infinite set of things, without literall...

Cruxes for AI Control via Proof Carrying Code at the End of 2025