You write the spec. The AI writes the code and the proof. The checker decides.

How to write specifications for AI-generated code and accept the agent's work mechanically, with a proof checker instead of trust.