This talk will cover three emerging trends at the intersection of AI and formal verification, and their interplay.

(1) In formal verification of software, we are accustomed to scarcity of expert practitioners, from whom a lot of hours are required to create verified software, resulting in a relatively small amount of the world’s software actually being verified, even within critical infrastructure sectors. As LLMs advance in general coding abilities, we are also seeing increasing ability to construct formal proofs, including for software verification subgoals that could not previously be automated. Given the exponential trends at play, we should expect at least a 10-100x decrease in expert hours required to construct verified software over the next few years, resulting in greatly increased adoption and Jevons-paradoxical increase in demand for experts in the least mechanizable skills, especially specification review.

(2) Increasingly powerful AI systems trained with reinforcement learning from feedback from so-called verifiers, which test Python code or the like, are increasingly cheating. It may soon become crucial to incorporate formal verifiers into the RL training process in order to continue pushing capabilities. The formal verification community should be eager to support this, because it will accelerate trend (1).

(3) Beyond the next few years, even if frontier AI systems are RL-trained only to solve formally verifiable problems, they may begin to cheat and dissemble at deployment-time in very dangerous ways, unless they are also *deployed* only to solve formally verifiable problems. This implies that we ought to expand the scope of formal verification to cyber-physical systems and beyond. We may take as a premise that AI may be able to solve nearly any NP problems that arise in practice, as long as we can actually supply correct certificate checkers for every such problem, and the *description length* of problems, solutions, and certificates is manageable (within LLM context windows). Expanding formal verification to cyber-physical systems with small neural control components is the purpose of the Safeguarded AI programme that I direct at UK ARIA.