Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking
Formal specification promises early error detection, explicit invariants, and correctness by design, yet its notational cost has kept it out of mainstream practice. We argue that AI removes much of that cost: natural language enriched with lightweight mathematics, written in \LaTeX, can serve as an intermediate specifi...