If we cannot specify it, we cannot govern it
AI systems are increasingly trusted to act, not just to answer. Our ability to check what they can actually do has not kept pace. Formal methods will not give us certainty, but they can force us to say precisely what a system must never do.
