My experience using coding agents to help formally verify the UK ATC meltdown solution in Lean.