The rapid advancement of artificial intelligence (AI) systems has created an urgent need to secure the infrastructure on which AI runs. In this report, the authors use results from a survey sent to experts in AI, formal methods, and other areas to determine whether formal methods—using mathematical techniques to reason about software behavior and, potentially, show that systems behave as specified—could meaningfully secure AI infrastructure.

Verified Machine Learning Infrastructure

Formal Methods for Trustworthy Artificial Intelligence Deployment

Gopal P. Sarma, Rachel Steratore, Sunny D. Bhatt, Geoffrey Irving

ResearchPublished Jun 4, 2026

Cover: Verified Machine Learning Infrastructure
Download PDF
Additional Downloads

Includes Annex: Survey Instrument

The rapid advancement of frontier artificial intelligence (AI) systems has created an urgent need to secure the infrastructure on which these systems run. As AI advances, so do its associated threats: Not only could malicious actors target AI infrastructure to steal model weights or disrupt operations, but a misaligned AI system could exploit vulnerabilities in its own infrastructure to bypass safety monitors or exfiltrate itself.

To address this possibility, the authors surveyed 23 experts in early 2026 to determine whether formal methods—using mathematical techniques to reason about software behavior and, potentially, show that systems behave as specified—could meaningfully reduce risks associated with AI infrastructure vulnerabilities. The survey respondents were experts in the domains of formal methods, AI infrastructure, cybersecurity, software engineering, hardware architecture, and policy.

Using responses from the survey, the authors examined which components of the machine learning inference and training stacks are most amenable to formal verification, what security properties could be guaranteed, what development and adoption barriers exist, and how advances in AI-assisted formal methods might change the calculus. The authors offer preliminary recommendations and a starting point for a community-technical roadmap oriented toward frontier AI labs, the formal methods community, hardware vendors, government agencies, and the broader public.

Key Takeaways

  • The vulnerability landscape is severe and poses significant risks. Critical vulnerabilities in major serving frameworks confirm that machine learning (ML) infrastructure has often prioritized performance and features over security. In the survey, experts rated weight integrity and supply chain threats as the most urgent concerns.
  • Verification is effective for infrastructure but not for models. Formal methods can address code-level correctness—memory safety, access control, protocol enforcement, sandbox isolation—but have limited reach into semantic challenges, such as model sandbagging or jailbreaks.
  • Focusing on cryptographic primitives and access control is the clear starting point. These components combine the highest-security value with the highest-verification feasibility. In fact, production-ready verified implementations already exist.
  • The graphics processing unit (GPU) verification gap is significant but narrowing. There are no mature full-stack formal semantics for major GPU programming frameworks, although partial formal-semantics work exists, and advances in this area suggest that automated GPU kernel verification is becoming more tractable.
  • AI-assisted formal methods are the critical enabler. There was near-unanimous agreement that AI will dramatically reduce the cost of proof syntheses and repairs. However, experts warned that AI-generated specifications are vulnerable to subtle flaws that cannot be mechanically checked.
  • Adoption requires a value proposition beyond security. In a capability race, frontier labs will not accept meaningful performance or velocity penalties for security purposes alone. Verified infrastructure must be highlighted for its competitive advantages (e.g., fewer bugs, data-breach protection, regulatory positioning).

Recommendations

  • Frontier AI labs and hyperscalers should develop formal specifications for access control and safety monitor requirements (access control was among the highest-rated components for both security value and verification feasibility).
  • Frontier AI labs and hyperscalers should design systems that separate verified invariant-enforcing components from unverified performance-optimized code, thus enabling verification without sacrificing development velocity.
  • The formal methods community should engage with AI safety requirements to understand what properties matter most for ML infrastructure security.
  • The formal methods community should develop benchmarks for AI-assisted systems verification, particularly benchmarks targeting proof repair and systems-level reasoning about memory, state, and concurrency.
  • The formal methods community should create verification approaches that accommodate rapidly evolving codebases by separating verified security-enforcement components from unverified performance-optimized code.
  • Hardware vendors should publish formal semantics or verifiable interfaces for hardware instruction set architectures and memory models.
  • Government agencies should consider procurement requirements for verified components in high-assurance AI applications.

Topics

Document Details

Citation

Chicago Manual of Style

Sarma, Gopal P., Rachel Steratore, Sunny D. Bhatt, and Geoffrey Irving, Verified Machine Learning Infrastructure: Formal Methods for Trustworthy Artificial Intelligence Deployment. Santa Monica, CA: RAND Corporation, 2026. https://www.rand.org/pubs/research_reports/RRA4881-1.html.
BibTeX RIS

Research conducted by

This research was independently initiated and conducted by the Center on AI, Security, and Technology within RAND Global and Emerging Risks using income from operations and gifts and grants from philanthropic supporters.

This publication is part of the RAND research report series. Research reports present research findings and objective analysis that address the challenges facing the public and private sectors. All RAND research reports undergo rigorous peer review to ensure high standards for research quality and objectivity.

This document and trademark(s) contained herein are protected by law. This representation of RAND intellectual property is provided for noncommercial use only. Unauthorized posting of this publication online is prohibited; linking directly to this product page is encouraged. Permission is required from RAND to reproduce, or reuse in another form, any of its research documents for commercial purposes. For information on reprint and reuse permissions, please visit www.rand.org/pubs/permissions.

RAND is a nonprofit institution that helps improve policy and decisionmaking through research and analysis. RAND's publications do not necessarily reflect the opinions of its research clients and sponsors.