Beneficial AI Foundation (BAIF)

Theory of Change

BAIF's stated mission: "No one knows how to make tomorrow's AI safe. Let's change that." The causal chain: develop quantitative safety guarantees for AI systems using formal verification, analogous to how the FDA requires quantitative evidence of drug side effects and the FAA requires bounds on engine failure rates.

This takes its strongest form in Tegmark and Omohundro's September 2023 paper, which argues that "proof-carrying AGI running on proof-carrying hardware appears to be the only hope for a guaranteed solution to the control problem." The broader Guaranteed Safe AI (GSAI) framework paper (Dalrymple, Tegmark, Bengio, Russell et al., May 2024) softens this to a "family of approaches" using three components: a world model, a safety specification, and a verifier that provides "an auditable proof certificate."

Tegmark connects this technical agenda to a policy vision: an "FDA for AI" where companies must demonstrate safety before deploying powerful systems. In his October 2023 Senate testimony: "If a person or organization wants to be sure that their AGI never lies, never escapes and never invents bioweapons, they need to impose those requirements and never run versions that don't provably obey them."

What They Do

BAIF's primary concrete output is the Buterin AI Existential Safety Fellowship, co-managed with the Future of Life Institute. Since 2022, the program has funded 19+ PhD students ($40K/yr + tuition for 5 years + $10K research fund) and postdocs ($80K/yr + $10K research fund) at major universities. Notable fellows include Peter Park (AI deception survey, Nature coverage), Stephen Casper (red-teaming, RLHF limitations), and Caspar Oesterheld (game theory and AI). Applications for 2026 are open.

The fellowship includes an unusual anti-lab-pipeline clause: fellows who join frontier AI companies (Anthropic, Google DeepMind, Meta, OpenAI, xAI) within 2 years must donate half their gross compensation to charity.

In-house research is limited. The only confirmed BAIF researcher, Alok Singh (formerly Lawrence Berkeley National Lab), published "Vericoding" (Sept 2025) -- a benchmark of 12,504 formal specifications for verified program synthesis. BAIF's GitHub has 121 public repositories focused on Lean 4 formal verification tools.

QAISI (Quantitative AI Safety Initiative) lists seven prominent research leads -- Clark Barrett (Stanford), Yoshua Bengio (Mila), Steve Omohundro, Bryan Parno (CMU), Stuart Russell (Berkeley), Dawn Song (Berkeley), Max Tegmark (MIT) -- but has produced zero publications under the QAISI banner. These are advisory affiliations at home institutions, not employment relationships with BAIF.

BAIF organized events including the MIT Mechanistic Interpretability Conference (2023), ICML MI Workshop (2024), and Berkeley Proof Scaling Workshop.

Key People

Max Tegmark -- President and Treasurer. MIT physics professor, FLI co-founder and president, FQXi scientific director, Improve the News Foundation co-founder. Author of Life 3.0. Named Time 100 AI (2023). Receives $0 from BAIF; his $457,840 compensation is from MIT. He simultaneously leads at least 5 organizations, raising questions about time allocation to BAIF specifically.

Meia Chita-Tegmark -- Secretary. Tegmark's wife. FLI co-founder. Psychology PhD (Boston University), teaches AI ethics at Tufts. Human-robot interaction researcher.

Alok Singh -- Only confirmed in-house researcher. Former Lawrence Berkeley National Lab (2019-2024). Works on Lean 4 + AI formal verification.

Team size is very small -- likely 1-2 staff plus the Tegmark couple as uncompensated officers. Both the /team and /fellows pages on the website return 404 errors.

Money and Incentives

Revenue: $0 (2022, founding year), $1,865,000 (2023, all contributions), $125,000 (2024). Revenue collapsed 93% from 2023 to 2024 with no public explanation.

Expenses: $821 (2022), $644,009 (2023). Zero salaries or wages in all years. The $644K in expenses is unexplained -- possible destinations include fellowship disbursements, contractor payments, and events.

Assets: $1,230,297 (2023), declining to $720,808 (2024). At 2023 expense rates, BAIF has roughly 1 year of runway.

Donors: Vitalik Buterin (Ethereum co-founder) and Erik Otto (Ethagi founder). BAIF receives zero funding from Coefficient Giving / Open Philanthropy. It is entirely outside the standard EA funding ecosystem.

Relationship to FLI: BAIF's sister organization, FLI (also founded by Tegmark), holds a ~$500M endowment from Buterin's 2021 SHIB donation. The Buterin Fellowship page lives on FLI's website and is described as "run in partnership." With 19+ fellows requiring potentially $1M+/yr in funding, and BAIF's 2024 revenue at only $125K, FLI is likely the primary funder. The financial flow between the two entities is undisclosed.

Donor risk: Buterin publicly criticized FLI's political pivot in March 2026, calling it potentially "authoritarian" and "fragile." He warned that FLI's regulation-first approach "VERY EASILY backfires." This creates uncertainty about future funding for the Tegmark ecosystem.

Business model: Pure donations from crypto-wealthy individuals. No product revenue, no government contracts, no EA funder oversight. This gives BAIF unusual independence but also unusual fragility.

Governance: BAIF has only two officers -- a married couple. No independent board. No advisory board. No public conflict-of-interest policy. Both officers receive $0 compensation from BAIF.

What Others Say

The core technical critique comes from Andrew Dickson's "Limitations on Formal Verification for AI Safety" (August 2024): Mathematical proofs work on symbol systems, not the physical world. The Mars Perseverance rover's formally verified software only covered ~20% of mission failure risk -- the 80% from physical causes remained unaddressed. Modeling whether a DNA sequence is harmful to humans would require "centuries" of progress in computational biology. "Our default stance as engineers and computer scientists should be skepticism."

Practitioner objection: Zac Hatfield-Dodds (FAR.AI talk, Hypothesis testing library maintainer): "Model weights are just completely intractable to reason about... The GSAI framework hasn't actually solved the problem, you've just moved it around -- now you have to convince me that the world model sufficiently accurately matches the real world." He also argues Tool AI is "unstable" because a trivial for-loop converts any tool into an agent.

The GSAI authors' response (Skalse et al., January 2025) retreats to a more modest position: GSAI "is not proposing to be a solution to ambitious alignment" but to "safety engineering applied to ASL-4 AI." They argue sound overapproximation is achievable without perfect world models, and even short-horizon guarantees are useful. This is more defensible than Tegmark's "only path" framing, but much less distinctive.

Dean Ball (Foundation for American Innovation, former Trump White House advisor) in debate with Tegmark: The FDA analogy breaks down because AI is a general-purpose technology. Preemptive regulation risks regulatory capture by incumbents. His P(doom) is 0.01% versus Tegmark's 90%+ -- a fundamental disagreement about whether this work is necessary at all.

ARIA's Safeguarded AI program (davidad/David Dalrymple, $80M UK government funding) is pursuing the same approach with 40x BAIF's peak budget: using frontier AI to develop formally verified control algorithms for critical infrastructure. ARIA's existence both validates the research direction and raises the question of whether BAIF is redundant.

What's Absent

No public explanation for why BAIF was created as a separate entity from FLI. Timing coincides with the Nya Dagbladet controversy (Dec 2022 founding, Jan 2023 controversy).
No QAISI-branded publications despite listing seven prominent research leads.
No explanation for the 93% revenue collapse from 2023 to 2024.
No disclosure of financial flows between FLI and BAIF.
No independent board members -- only a married couple as officers.
No public accounting of fellowship outcomes (publications, career trajectories, impact).
Zero community discussion of BAIF as an organization on LessWrong, EA Forum, or Alignment Forum.
No positioning relative to ARIA's $80M Safeguarded AI program pursuing the same approach.