A practical introduction to TLA+, why it matters for agentic coding, and how AI could take formal verification from models to machine-checked proofs and ultimately to verified software.