RESIThe Institute for
Responsible SuperintelligenceSupport RESI

How can we formally define and implement AI safety?

RESI focuses on the formal and design-oriented foundations of AI safety: precise safety objectives, explicit assumptions, mechanisms with analyzable guarantees, composition, and impossibility results.

Guarantees depend on stated assumptions about the system and adversary. They do not establish the safety of an entire AI system.

Our goal is to build approaches that develop together with systems as they become superintelligent.

Research at RESI is AI-assisted from the start, with AI-generated suggestions subject to independent examination and testing. We will develop and continually improve tools and workflows that use frontier AI agents at every stage, expanding the ideas and approaches our team can investigate.

Meet the team Support our work

Research outputs

Across our research areas, we pursue the following outputs:

  • Models, definitions, and impossibility results

    Develop models and precise definitions for AI safety.

    Establish where guarantees are impossible under stated assumptions.

  • Mechanisms and composition

    Develop mechanisms, protocols, and architectures that provide useful guarantees, and study whether those guarantees survive composition into larger systems involving models, tools, people, and institutions.

  • Implementations and proofs of concept

    Build implementations and proofs of concept. Where implementation requires resources beyond RESI’s capacity, share proofs of concept that frontier AI developers can evaluate and adopt.

Definitions and constructions develop together: a new protocol may reveal the right concept, and an impossibility result may show that a problem must be reformulated.

Research areas

These questions describe our key focus areas. In each area we pursue clear outputs that include definitions, mechanisms, working demonstrations, and results on what can and cannot be guaranteed.

Verification and oversight

What can a less capable overseer reliably verify about a more capable AI’s properties, answers, and actions without reproducing all of the system’s work?

A useful verification method must state which claims it can check, put bounds on how often it can be wrong, and set reasonable bounds on the resources its verifier needs. In mathematics, there are exact definitions of correct and incorrect statements and what constitutes a proof. For the open-ended answers generated by modern AI systems in many other fields, we need to define anew what counts as sufficient evidence and how to evaluate it before letting the system take action.

We collaborate on this area through the Cryptographic verification working group, led by Shafi Goldwasser.

Control and delegation

What authority can we delegate to AI while preserving our ability to intervene as AI becomes more intelligent than us?

Explore protocols that make the scope of a delegated task explicit: which tools may be used, which actions require approval, and when execution should stop. Guarantees should account for the environment and the power of the user, not just the AI model.

We collaborate on this area through the Monitoring and control working group, led by Vinod Vaikuntanathan.

Composition

Which safety properties can be better achieved when connections between models, tools, and agents are limited?

A property established for one component may fail when it interacts with another. Study interfaces, shared resources, patterns of interaction, and assumptions under which local guarantees support a claim about an entire system, as well as constructions that show when composition is impossible.

We collaborate on this area through the Modular architectures working group, led by Adam Tauman Kalai.

Shaping multi-agent dynamics

How should we design agents and structure their interactions to build safe multi-agent systems with provable guarantees?

Behavior of an AI system often emerges from complex interactions between many agents (swarms). These agents cooperate, compete, assume roles, and communicate to further their individual or shared goals. Though swarms of agents have emerged only recently, the problem of constraining and shaping the dynamics of interacting parties is well studied in other settings. We draw on ideas from game theory, distributed computing, social psychology, and law to govern these dynamics and achieve desirable outcomes.

We collaborate on this area through the Game-theoretic foundations of AI safety working group, led by Yannai A. Gonczarowski.

Formal verification

How can formal verification enable powerful AI throughout software development without creating new risks of cyberattacks or otherwise dangerous behavior?

Develop mathematical proofs that the software surrounding AI enforces safety constraints, including containment that holds regardless of a model’s internal decisions. The scope extends from securing conventional computing infrastructure to verifying the hardware and software that run deep learning, and ultimately to systems that repeatedly improve themselves. Alongside these technical problems, study how to organize and equip researchers to produce the necessary proofs before the risks materialize.

We collaborate on this area through the Formal verification working group, led by Adam Chlipala.

Impossibility as a safety result

What limits on technologically achievable safety guarantees can be proved, and how can those limits inform which laws, policies, and regulations must be adopted?

Not all safety goals are achievable, and sometimes provably so. Understanding these limits can help policymakers identify requirements that cannot be satisfied together, justify imposing restrictions, and clarify what access auditors need to assess safety claims.

Leveraging AI for AI safety research

How can we use AI to develop new AI safety concepts, definitions, insights, and formal guarantees?

As AI grows smarter, it gains a greater capacity to act in unanticipated ways and to cause harm despite human safeguards. For humans to keep pace, we must use AI wisely as a tool to improve and accelerate AI safety research. This includes exploring whether recent developments in AI-assisted mathematics can accelerate the creation of mathematical foundations for AI safety.

We collaborate on this area through the AI harnesses working group, led by Jonathan Shafer.

Incentives and institutions

How should incentives work alongside technical safeguards?

Technical mechanisms operate within organizations, markets, and legal institutions. Model those interactions and assess which guarantees remain useful when the people and systems involved have different objectives, and under what assumptions.

We collaborate on this area through the Game-theoretic foundations of AI safety working group, led by Yannai A. Gonczarowski.

Cryptography and security

How do we repurpose cryptographic tools for secrecy, authentication, multi-party secure computation and obfuscation to navigate the AI multi-agentic world?

Cryptography studies how parties can compute and communicate securely even when some behave maliciously. For AI agents, we need to model agents capabilities and adversary agents completely differently to protect users. Each traditional cryptographic goal requires a new precise model of the adversary's computational power, information, and ability to collude as well as a proof of security.

We collaborate on this area through the Cryptography and cybersecurity working group, led by Yaron Singer.

Legal alignment

How can legal constructs be leveraged to develop technical methods for building safe by design superintelligence?

Explore how the law’s concepts, principles, and institutions can serve as a blueprint to propose technical methods for robustly safe AI systems -- and develop theoretical and empirical case studies of such legal alignment.

We collaborate on this area through the Legal alignment working group, led by Noam Kolt.

Attribution

Can we attribute model decisions to training data?

The map from training data or information in large contexts can be opaque. Tools for disentangling the effects of these kinds of information on the behavior of AIs could serve as essential tools for interpretability and safety, but at present, all such tools are heuristic and unverifiable. If we want to fully understand AI behavior, we need reliable and rigorous ways to trace model decisions and outputs back to data.

We collaborate on this area through the Data attribution working group, led by Sam Gunn.

Working groups

Working groups bring RESI researchers together to develop research outputs across our key research areas. They open new directions and revisit classical questions in light of superintelligence. Each group is organized by one or more leaders who decide on its structure. Alongside working groups, RESI co-hosts seminars with MIT on the foundations of AI safety.

  • Game-theoretic foundations of AI safety

    Led by Yannai A. Gonczarowski

    details

    Investigates multi-agent AI alignment through game-theoretic and economic tools, asking where those tools are appropriate and where new ones are needed.

    Foundational research: Algorithmic Collusion by Large Language Models

  • Cryptographic verification

    Led by Shafi Goldwasser

    details

    Develops methods that enable AI systems to provide convincing evidence that their answers meet appropriate standards of correctness. Mathematical claims may admit independently checked proofs; other domains require task-appropriate standards of correctness.

    Related foundational research: A Theory for Worst-Case vs. Average-Case Guarantees for LLMs

  • Modular architectures

    Led by Adam Tauman Kalai

    details

    Studies how restricted modules, used alone or in structured interactions, can make AI systems safer by limiting what each component can do. Could a constrained component control spending while a more capable model proposes actions without direct access to payment credentials?

    Related foundational research: Consensus Sampling for Safer Generative AI

  • Monitoring and control

    Led by Vinod Vaikuntanathan

    details

    Investigates when monitoring can detect subversive behavior in AI models and agents, where it falls short, and what additional controls may be needed.

  • AI harnesses

    Led by Jonathan Shafer

    details

    Investigates how frontier AI can assist with definitions, conjectures, proofs, counterexamples, and experiments.

  • Led by Noam Kolt

    details

    Explores how legal constructs such as separation of powers, corporate governance, and fiduciary duties can inform technical approaches to safe by design superintelligence. One proposed direction is a theoretical or empirical case study of a legal construct adapted to a technical alignment problem. The focus is on using legal ideas to improve alignment, rather than primarily on applying existing legal doctrine to AI.

    Foundational research: Superintelligence and Law · Legal Alignment for Safe and Ethical AI

  • Formal verification

    Led by Adam Chlipala

    details

    Adam Chlipala's announced agenda asks how formal verification could support powerful AI in software development while reducing security risks. It distinguishes general software infrastructure, AI-specific infrastructure, and recursively self-improving systems. The agenda addresses both technical questions and how to organize the work, including which directions are ready to pursue.

    Read the announcement on LessWrong

  • Cryptography and cybersecurity

    Led by Yaron Singer

    details

    Uses mathematical foundations and modeling to study how to secure AI applications, protect against AI-generated attacks, and use AI to improve cyber defenses.

  • Ethics and superintelligence

    Led by Chloé Bakalar

    details

    Examines fairness, human control, and the distribution of resources in a world with superintelligent AI.

  • Data attribution

    Led by Sam Gunn

    details

    Studies how to attribute model behavior to subsets of training data with provable guarantees under concrete, realistic assumptions. Proposed directions include inference-time attribution, lower bounds, experimental tests of attribution schemes, and adaptive attribution queries.

    Foundational research: How to sketch a learning algorithm

  • AI safety using quantum effects

    Led by Greg Gluch

    details

    Investigates whether quantum resources could support restrictions on access, reuse, or revocation of AI capabilities that classical software alone cannot provide.

Meet the team

Foundational research by the RESI team

The papers below are prior work by researchers now associated with RESI.

  • Evaluating large language models for accuracy incentivizes hallucinations

    Nature · 2026Details Adam Tauman Kalai, Ofir Nachum, Santosh S. Vempala, Edwin Zhang
    Why language models hallucinateWhy do models guess instead of admitting uncertainty? This work analyzes how training and evaluation reward guessing, and argues for scoring systems that make acknowledging uncertainty a better strategy.Changing the scoring rule is not a guarantee that hallucinations disappear.

  • A Theory for Worst-Case vs. Average-Case Guarantees for LLMs

    NeurIPS · 2025Details Noga Amit, Shafi Goldwasser, Orr Paradise, Guy N. Rothblum
    Models that can prove their answersA framework for learning models that supply interactive proofs of their outputs. Demonstrated on greatest-common-divisor computation, not unrestricted natural-language answers.

  • How to Avoid Debate: Scalable AI Safety via Doubly-Efficient Interactive Proofs

    ICML · 2026Details L. Chen, Y. Tauman Kalai, Z. Xi
    Develops methods for checking certain computations that use external information, such as database records or human judgments. The guarantees require specific structure in that information or computations that tolerate a limited number of errors.

  • BarrierNet: Differentiable Control Barrier Functions for Learning of Safe Robot Control

    IEEE Transactions on Robotics · 2023Details W. Xiao, T.-H. Wang, R. Hasani, M. Chahine, A. Amini, X. Li, D. Rus
    Introduces a trainable safety layer that constrains a robot’s actions to satisfy specified requirements, with guarantees that depend on the model of the robot and its environment.

  • Consensus Sampling for Safer Generative AI

    Presented at IASEAI · 2026Details A. Kalai, Y. Tauman Kalai, O. Zamir
    Selects an output from several models, or declines to answer, with a provable limit on the risk of harmful output relative to the more reliable models. The method requires access to each model’s output probabilities. Producing useful answers also depends on sufficient overlap among the reliable models’ output distributions.

  • Governing AI Agents

    Notre Dame Law Review · 2026Details N. Kolt
    Examines the responsibilities and limits of authority that arise when AI agents act for people, and explains why existing approaches to monitoring and accountability may be insufficient.

  • On the Impossibility of Separating Intelligence from Judgment: The Computational Intractability of Filtering for AI Alignment

    ICLR · 2026Details S. Ball, G. Gluch, S. Goldwasser, F. Kreuter, O. Reingold, G. Rothblum
    Understanding the limits of filteringCryptographic constructions expose computational limits of certain input and output filters. The results depend on explicit hardness assumptions and formal settings.Establishes computational barriers to external prompt and output filtering under cryptographic hardness assumptions and specified relationships between the model and filter. These worst-case results do not say that filtering has no practical value.

  • Planting Undetectable Backdoors in Machine Learning Models

    FOCS · 2022Details S. Goldwasser, M. Kim, V. Vaikuntanathan, O. Zamir
    Shows how a model can appear to function normally while containing a hidden trigger that changes its behavior. Under cryptographic assumptions, such backdoors can evade inspection within feasible computing limits.

  • A Cryptographic Perspective on Mitigation vs. Detection in Machine Learning

    Preprint · 2025Details G. Gluch, S. Goldwasser
    Shows that, for certain tasks involving generated outputs, a defense can limit harmful behavior even when the harmful inputs cannot be efficiently identified.

  • Pseudorandom Error-Correcting Codes

    CRYPTO · 2024Details M. Christ, S. Gunn
    Introduces a way to hide information in apparently random data while allowing a key holder to recover it after specified alterations. This underpins methods for watermarking AI-generated content and hiding communication.

  • Oblivious Defense in ML Models: Backdoor Removal without Detection

    STOC · 2025Details Shafi Goldwasser, Jonathan Shafer, Neekon Vafa, Vinod Vaikuntanathan
    Defense without detectionCan a defense work without identifying an attack? This work gives backdoor-mitigation guarantees under assumptions about the ground-truth function.Develops methods for neutralizing hidden triggers that alter a model’s behavior, without first detecting them.Scope. The guarantees apply to learning tasks with specified mathematical structure in the ground-truth function.

  • Undetectable Conversations Between AI Agents via Pseudorandom Noise-Resilient Key Exchange

    FOCS · 2026 · AcceptedDetails Vinod Vaikuntanathan, Or Zamir
    The limits of transcript auditingCan ordinary exchanges conceal a second conversation? Under stated cryptographic and entropy assumptions, this work constructs covert communication between agents with no pre-shared secret, revealing limits of passive transcript auditing.Shows how cooperating AI agents could hide secret exchanges within ordinary-looking messages, even without a shared secret at the outset.Scope. The construction assumes cryptographic hardness and sufficient entropy in messages, and concerns passive transcript auditing.

  • Algorithmic Collusion by Large Language Models

    EC · 2026Details S. Fish, Y. A. Gonczarowski, R. I. Shorrer
    Experiments show that pricing agents based on large language models can reach prices above competitive levels, with outcomes sensitive to changes in their instructions.

  • Superintelligence and Law

    Harvard Journal of Law & Technology · Forthcoming (preprint 2026)Details N. Kolt
    Sets out how AI agents acting autonomously become subjects of law, users of legal instruments such as contracts and courts, and in time writers and enforcers of law, and which assumptions in legal theory and doctrine that calls into question.

  • Legal Alignment for Safe and Ethical AI

    TMLR · 2026Details N. Kolt et al
    Surveys how legal rules, principles and methods can be used to specify how AI systems should act and to inform their design, and sets out three research pathways for doing so.

  • How to sketch a learning algorithm

    Preprint · 2026Details Sam Gunn
    Experimental codeData deletion and attributionHow would a model behave if some training data had been left out? A sketch of the learning algorithm predicts these counterfactual outputs, supporting data deletion queries and attribution, with error and failure guarantees under a stability assumption.The method predicts counterfactual measurements rather than outputting a retrained model. Evidence for the stability assumption comes from small-scale microgpt experiments.