Provably Safe AI (davidad agenda)

Overview

Provably Safe AI represents one of the most ambitious research agendas in AI safety: designing advanced AI systems where safety is guaranteed by mathematical construction rather than verified through empirical testing. Led primarily by David "davidad" Dalrymple---the youngest-ever MIT graduate degree recipient at age 16, former Filecoin co-inventor, and current Programme Director at ARIA---this agenda seeks to create AI systems whose safety properties can be formally proven before deployment, potentially enabling safe development even of superintelligent systems.

The foundational paper Towards Guaranteed Safe AI↗📄 paper★★★☆☆arXivTowards Guaranteed Safe AIDavid "davidad" Dalrymple, Joar Skalse, Yoshua Bengio et al. (2024)safetyinner-alignmentdistribution-shiftcapability-generalizationSource ↗, published in May 2024 by Dalrymple, Joar Skalse, and co-authors 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 is a UC Berkeley professor who founded CHAI in 2016 with $5.6M from Coefficient Giving (then Open Philanthropy) and authored 'Human Compatible' (2019), which proposes cooperative inv...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, and Sanjit Seshia, introduces the core framework of "guaranteed safe (GS) AI." The approach requires three components: a world model (mathematical description of how the AI affects the outside world), a safety specification (mathematical description of acceptable effects), and a verifier (auditable proof certificate that the AI satisfies the specification relative to the world model).

The core insight motivating this work is that current AI safety approaches fundamentally rely on empirical testing and behavioral observation, which may be insufficient for systems capable of strategic deception or operating in novel circumstances. If we could instead construct AI systems where safety properties are mathematically guaranteed, we could have much stronger assurance that these properties will hold regardless of the system's capabilities or intentions. This parallels how we trust airplanes because their structural properties are verified through engineering analysis, not just flight testing. Crucially, this approach does not require interpretability to be solved and could still rule out deceptive alignment.

The agenda faces extraordinary technical challenges. It requires solving multiple hard problems including: constructing formal world models that accurately represent relevant aspects of reality, specifying human values in mathematically precise terms, building AI systems that can reason within these formal frameworks, and proving that the resulting systems satisfy desired safety properties. Many researchers consider one or more of these components to be fundamentally intractable. However, proponents argue that even partial progress could provide valuable safety assurances, and that the potential payoff justifies significant research investment.

Risk Assessment & Impact

How It Works

The Guaranteed Safe AI framework operates through a verification pipeline that checks every action before execution:

The key insight is that the proof checker can be much simpler than the proof generator. While generating proofs of safety may require sophisticated AI reasoning, verifying those proofs can be done by a small, formally verified checker---similar to how a calculator can verify a proof even if generating it requires human creativity.

The davidad Agenda

Core Components

Key Technical Requirements

ARIA Programme Structure

ARIA's Safeguarded AI programme is the primary funder of provably safe AI research globally. The programme aims to develop quantitative safety guarantees for AI "in the way we have come to expect for nuclear power and passenger aviation."

Programme Overview

Research Themes

Technical Approach

World Model Requirements

Value Specification Approaches

Proof-Based Safety

Feasibility Assessment

Optimistic View

Proponents point to the remarkable success of formal verification in other domains. CompCert, a formally verified C compiler, was tested for six CPU-years by the Csmith random testing tool without finding a single wrong-code error---the only compiler tested for which this was true. seL4, a formally verified operating system microkernel, has machine-checked mathematical proofs for Arm, RISC-V, and Intel architectures and is used in aerospace, autonomous aviation, and IoT platforms. These demonstrate that formal verification can scale to real systems.

Skeptical View

Key Uncertainties

Comparison with Related Approaches

Scalability Assessment

Quick Assessment

Risks Addressed

If successful, provably safe AI would provide mathematical guarantees against several core AI safety risks:

Current State

As of early 2025, provably safe AI remains in the early research phase with no working prototypes:

The International Neural Network Verification Competition represents related work on verifying properties of neural networks, with tools like α,β-CROWN achieving significant speedups over traditional algorithms. However, this work addresses a narrower problem than full GS AI.

Limitations

• May Be Impossible: Core components may be fundamentally intractable
• Capability Tax: Constraints may make systems unusable
• World Model Problem: Cannot formally specify reality comprehensively
• Value Specification Problem: Human values resist precise formalization
• Long Timeline: Decades of research may be needed
• Alternative Approaches May Suffice: Empirical safety might be enough
• Verification Complexity: Proofs may be too expensive to generate

Open Questions

Sources & Resources

Key Documents

Key Organizations

Formal Verification Precedents

AI Transition Model Context

Provably safe AI affects the Ai Transition Model through fundamental safety guarantees:

The provably safe AI agenda represents a moonshot approach that could fundamentally solve AI safety if successful. The extreme difficulty of the technical challenges means success is uncertain, but the potential value of even partial progress justifies significant research investment. This approach is particularly valuable as a complement to empirical safety work, providing a fundamentally different path to safe AI.