Using algebra and LLMs to verify a flight-plan bug fix in Lean

This blog post discusses the use of formal verification in software development, particularly in relation to a real-world bug fix from the 2023 UK air traffic control incident. It explores how LLM coding agents could make the process of formal verification more accessible by restating bugs in algebraic terms, highlighting the strengths and weaknesses of LLMs in this context.