Tests and types are our correctness gates. But who verifies the gates themselves? With agentic codegen flooding our pipelines with code we didn't write, that question has never been more dangerous to ignore. In this talk, we explore how theorem provers complement existing practices, adding mathematical certainty where it matters most.