Tag
A developer uses LLMs and algebraic reformulation to formally verify a bug fix for the 2023 UK air traffic control meltdown in the Lean proof assistant, finding that LLMs are great at grinding proofs but poor at specifications.