Provable / Guaranteed Safe AI

Quick Assessment

Key Links

Overview

Provable or "Guaranteed Safe" AI refers to approaches that aim to build AI systems with mathematical safety guarantees rather than empirical safety measures. The core premise is that we should be able to prove that an AI system will behave safely, not merely hope based on testing.

The most prominent current effort is Davidad's Open Agency Architecture, funded through the UK's ARIA (Advanced Research + Invention Agency) programme. This approach represents a fundamentally different philosophy from mainstream AI development: safety through formal verificationApproachFormal Verification (AI Safety)Formal verification seeks mathematical proofs of AI safety properties but faces a ~100,000x scale gap between verified systems (~10k parameters) and frontier models (~1.7T parameters). While offeri...Quality: 65/100 rather than alignment through training.

Estimated probability of being dominant at transformative AI: 1-5%. This is ambitious and faces significant scalability questions, but offers uniquely strong safety properties if achievable.

Formal Verification Approaches

The field of guaranteed safe AI encompasses multiple verification methodologies, each with different tradeoffs between expressiveness, scalability, and the strength of guarantees provided.

flowchart TB
  subgraph approaches["Guaranteed Safe AI Approaches"]
      direction TB
      subgraph formal["Formal Verification"]
          smt["SMT-Based<br/>(Satisfiability Modulo Theories)"]
          abstract["Abstract Interpretation"]
          bound["Bound Propagation<br/>(α,β-CROWN)"]
      end

      subgraph hybrid["Hybrid Approaches"]
          neuro["Neuro-Symbolic<br/>Integration"]
          shield["Verification-Guided<br/>Shielding"]
          runtime["Runtime<br/>Monitoring"]
      end

      subgraph world["World Model Approaches"]
          physics["Physics-Based<br/>Simulators"]
          causal["Causal<br/>Models"]
          probabilistic["Probabilistic<br/>Programs"]
      end
  end

  subgraph guarantees["Safety Guarantee Types"]
      local["Local Robustness<br/>(perturbation bounds)"]
      global["Global Properties<br/>(invariants)"]
      temporal["Temporal Properties<br/>(always/eventually)"]
  end

  formal --> local
  formal --> global
  hybrid --> temporal
  world --> global

  style approaches fill:#e8f4e8
  style guarantees fill:#fff3e0

Verification Methodology Comparison

VNN-COMP 2024 Results

The 5th International Verification of Neural Networks Competition (VNN-COMP 2024) provides the most recent benchmarks for the field:

Key finding: The best tools can now verify local robustness properties on networks with millions of parameters in reasonable time, but this remains 6 orders of magnitude below frontier model scale.

Conceptual Framework

flowchart TB
  subgraph world["World Model (Verified)"]
      physics["Physics Simulator"]
      state["State Representation"]
      predict["Prediction Engine"]
  end

  subgraph agent["Agent (Bounded)"]
      goals["Formal Goal Spec"]
      planner["Verified Planner"]
      bounds["Safety Bounds"]
  end

  subgraph verify["Verification Layer"]
      proofs["Safety Proofs"]
      monitor["Runtime Monitor"]
      audit["Audit Trail"]
  end

  goals --> planner
  planner --> world
  world --> predict
  predict --> bounds
  bounds --> proofs
  proofs --> monitor
  monitor --> |"Safe Action"| output["Output"]

Key Properties

ARIA's Safeguarded AI Programme

The UK's Advanced Research + Invention Agency (ARIA) has committed £59 millionTotal Funding Raised£59 millionAs of: Nov 2025GBP 59M total Safeguarded AI programme budget across all technical areas (TA1.1: GBP 3.5M/22 projects, TA1.2+1.3: GBP 14.2M, TA1.4: GBP 3.4M, TA2: GBP 1M Phase 1, TA3: GBP 5.4M/9 projects). Value in GBP not USD.Source: aria.org.uksid_XqjV4mbMXQ.total-funding → over 3-5 years to the Safeguarded AI programme, led by Programme Director David "davidad" Dalrymple with Scientific Director Yoshua BengioPersonYoshua BengioComprehensive biographical overview of Yoshua Bengio's transition from deep learning pioneer (Turing Award 2018) to AI safety advocate, documenting his 2020 pivot at Mila toward safety research, co...Quality: 39/100 (joined August 2024). This represents the largest government investment specifically targeting provably safe AI. In November 2025, ARIA announced a significant pivot: TA1's scope was expanded to broader "mathematical assurance and auditability"; TA2 Phase 2 (the £18M "AI Production Facility") was abandoned as frontier AI advances made dedicated ML capability development less valuable; and TA3 Phase 2 (£8.4M) was cancelled and replaced by a cybersecurity focus on formally-verified firewalls for critical infrastructure. Kathleen Fisher (former DARPA HACMS programme lead) is incoming as ARIA CEO.

The Guaranteed Safe AI Framework

The foundational paper "Towards Guaranteed Safe AI" (May 2024) was co-authored by 17 prominent researchers including Yoshua BengioPersonYoshua BengioComprehensive biographical overview of Yoshua Bengio's transition from deep learning pioneer (Turing Award 2018) to AI safety advocate, documenting his 2020 pivot at Mila toward safety research, co...Quality: 39/100, Stuart RussellPersonStuart RussellStuart Russell (born 1962) is a British computer scientist and UC Berkeley professor who co-authored the dominant AI textbook 'Artificial Intelligence: A Modern Approach' (used in over 1,500 univer...Quality: 30/100, Max TegmarkPersonMax TegmarkComprehensive biographical profile of Max Tegmark covering his transition from cosmology to AI safety advocacy, his role founding the Future of Life Institute, and his controversial Mathematical Un...Quality: 63/100, Sanjit Seshia, Steve Omohundro, Christian Szegedy, Joe Halpern, Clark Barrett, Jeannette Wing, and Joshua Tenenbaum. It defines the core architecture:

Core Components

ARIA Programme Structure

Key quote from davidad: "The frontier model needs to submit a proof certificate, which is something that is written in a formal language that we're defining in another part of the program... This new language for proofs will hopefully be easy for frontier models to generate and then also easy for a deterministic, human-audited algorithm to check."

Key Technical Challenges

According to the Stanford Center for AI Safety whitepaper, the complexity and heterogeneity of AI systems means that formal verification of specifications is undecidable in general—even deciding whether a state of a linear hybrid system is reachable is undecidable.

Safety Implications

Advantages

Limitations and Risks

Research Landscape

Key Organizations

Key People

Key Publications

Comparison with Other Approaches

Probability Assessment

Quantified Probability Factors

Arguments for Higher Probability (greater than 5%)

1. Strong safety incentives - As AI gets more powerful, demand for guarantees may increase; International AI Safety Report 2025 emphasizes need for mathematical guarantees in safety-critical domains
2. Regulatory pressure - EU AI Act requires risk assessment for high-risk AI; formal verification may become compliance pathway
3. ARIA funding - £59MTotal Funding Raised£59 millionAs of: Nov 2025GBP 59M total Safeguarded AI programme budget across all technical areas (TA1.1: GBP 3.5M/22 projects, TA1.2+1.3: GBP 14.2M, TA1.4: GBP 3.4M, TA2: GBP 1M Phase 1, TA3: GBP 5.4M/9 projects). Value in GBP not USD.Source: aria.org.uksid_XqjV4mbMXQ.total-funding →+ committed with clear milestones; additional £110M in related ARIA funding in 2024
4. Compositionality - Verified components could be combined with other approaches; modular verification enables scaling

Arguments for Lower Probability (less than 1%)

1. Capability gap - Unverified systems may always be 10-100x more capable due to verification overhead
2. Speed of AI progress - TAI may arrive by 2030-2035; verification likely not ready
3. World model problem - Alignment Forum analysis shows verifying world models may be fundamentally impossible in open domains
4. Economic incentives - Labs optimizing for capabilities face 10-30% performance tax from verification requirements

Key Uncertainties

1. Can world models be verified? The entire approach depends on having provably accurate world models. This is the crux.

2. What's the capability ceiling? We don't know if verified systems can be competitive with unverified ones.

3. Can it handle novel situations? Formal verification typically requires known domains; how to handle unprecedented situations?

4. Will anyone adopt it? Even if possible, will competitive pressures prevent adoption?

Implications for Safety Research

This Approach Changes the Game If...

• World model verification is solved
• Verified systems reach capability parity
• Regulatory frameworks require formal safety proofs
• A major AI accident increases demand for guarantees

Research That Contributes

• Formal methods - Core verification techniques
• World modeling - Understanding physical systems
• Specification learning - Translating values to formal specs
• Compositional verification - Building larger proofs from smaller ones

Timeline Considerations

Historical Progress in Neural Network Verification

Critical observation: At the current rate of ~10x improvement every 3 years, verification tools will not reach frontier model scale until 2039-2042—potentially after transformative AI has already been developed via other paradigms.

Sources and Further Reading

• Dalrymple, D., et al. (2024). Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems. arXiv:2405.06624.
• Brix, C., Bak, S., Johnson, T., Wu, H. (2024). The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024). arXiv:2412.19985.
• ARIA. (2024). Safeguarded AI Programme Thesis v1.2.
• Huang, X., et al. (2024). A Survey of Safety and Trustworthiness of LLMs through V&V. Artificial Intelligence Review.
• Seshia, S., Sadigh, D., Sastry, S. (2017). Toward Verified Artificial Intelligence. Communications of the ACM.
• Stanford Center for AI Safety. Verified AI Whitepaper.
• International AI Safety Report. (2025). Second Key Update: Technical Safeguards and Risk Management.
• Fortune. (2025). Can AI be used to control safety critical systems?