Large language models can produce code faster than humans can audit it. They can also produce machine-checkable proofs with increasing success and speed. This changes the economics of a decades-old idea: an untrusted producer supplies executable code together with a proof that it satisfies a consumer-specified property, and an independent proof checker validates the proof. The resulting guarantee rests on the specification and the checker rather than on who wrote the code or which toolchain produced it.

A central challenge is carrying such guarantees end to end. Reasoning usually takes place at a high level of abstraction, but the guarantee must ultimately apply to the executable code that runs. In this talk, I examine two ways LLM-assisted verification can help close this gap. First, LLMs can reduce the cost of constructing and extending verified compilers, as illustrated by a recent case study in the CertiRocq compiler. However, this ties the guarantee to a single toolchain, whereas artifacts code often has heterogeneous provenance. A second route is to verify each executable artifact directly, proving that it refines a high-level program regardless of how the executable was produced. Can LLMs make this per-artifact approach practical?

I will present EquiVM, a Lean framework for stating and proving that deployed EVM bytecode refines a high-level program. We used EquiVM to evaluate the ability of frontier LLMs to produce refinement proofs for real deployed contracts as well as the cost in tokens and time. To date, LLM agents have completed, with minimal human guidance, proofs for 23 such contracts, including most of the MakerDAO stablecoin system. These results point toward a future in which correctness can be established for each executable artifact, rather than inherited from the toolchain that produced it. I conclude with lessons for designing verification infrastructure when machines produce the proofs.