Session Description

Tests and types are our correctness gates. Yet nobody verifies the gates themselves.
With agentic codegen flooding our pipelines at a scale we can’t keep up with, that gap has never been more dangerous to ignore.

This talk is about industrializing formal verification: taking theorem provers from an academical tool to a practical, deployable tool for production engineering teams.

We’ll look at how to identify the business logic that does: the invariants, state machines, and domain rules where a bug is not just an incident but a liability, how to scope verification to where it pays off and what are its limits.

Then we will see how to ship proven code. We will present ways to deploy verified code across backends, frontends, event-driven systems, and even embedded firmware, and what changes in your architecture and codebase when correctness is a certitude.

While writing proofs has been hard, writing a theorem statement is not. We’ll see how AI-augmented workflows let you specify what must be true, and let the machine figure out why it is. The result is a new kind of correctness gate: interfaces, in both the type-theory and software sense, that are proven contracts, not assumptions.

We started by questioning our gates. We’ll end with better ones.