Formal verification could help to secure critical software, but it faces a number of practical barriers. More advanced AI could help lift many, but not all, of them.