What happened
Published 4 June 2026 by RAND's Center on AI, Security, and Technology, this peer-reviewed research report surveys 23 experts across formal methods, AI infrastructure, cybersecurity, hardware architecture, and policy to assess whether mathematical verification techniques could meaningfully reduce risks in AI training and inference stacks. The central finding is that formal methods are technically feasible for specific, well-scoped components of ML infrastructure—particularly memory-management subsystems, hypervisors, and hardware-software interfaces—but face significant adoption barriers including toolchain immaturity, the stochastic nature of large model training, and lack of industry incentives. A novel dimension of the threat model is explicit: the report frames the risk not only as external adversaries stealing model weights, but as a misaligned AI system exploiting vulnerabilities in its own infrastructure to bypass safety monitors or exfiltrate itself. The authors offer a preliminary community-technical roadmap addressed to frontier AI labs, hardware vendors, formal-methods researchers, and government agencies.
Why it matters
For CISOs and AI security leads, this is the first RAND-credentialed survey to scope where formal verification is practically deployable in the AI stack today versus where it remains aspirational—directly informing infrastructure hardening priorities and vendor procurement criteria. The explicit inclusion of misaligned-AI self-exfiltration as a threat model elevates this beyond conventional cybersecurity framing.
Action needed
Circulate to the CISO and AI infrastructure team; use the report's component-level feasibility map to audit which layers of your own ML training and inference stack are candidates for formal verification controls, and flag gaps to your hardware and cloud vendors.