algebra

Formal verification has, until now, been a very laborious process. Therefore it is only considered for critical software, where bugs can cost lives or a lot of money. But LLM coding agents may be tipping the scales; formally verifying code might become viable for a much larger class of software. To test this, I picked a real bug, the 2023 UK air traffic control meltdown, and tried to prove a fix correct in Lean.

tl;dr: LLMs are not great at specs, excellent at grinding routine proofs, and the whole thing only became tractable once I restated the problem in algebraic terms.