Large language models can generate convincing code, but they cannot reliably determine whether it actually works. In this talk, I will demonstrate two ways to give AI an engineering feedback loop: a formal specification based on types and category theory, and a runtime verification system in which generated code is instrumented, executed, inspected, and corrected before it reaches the user.
We will travel from Aristotle’s syllogisms and Church encodings to TypeScript, advanced prompting, and AI-agent architecture. Finally, I will share how I tested these approaches at Avito, including correctness metrics, iteration count, token usage, latency, cost, and the practical limitations of automated verification.