Proof carrying contracts ensure ai agents keep agreements reliably
Proof-Carrying Contracts: Commitments AI Agents Cannot Break
Artificial IntelligenceCryptography and SecurityLogic in Computer ScienceMultiagent Systems
Summary
AI agents often make decisions and take actions for people or other agents, but text instructions alone cannot guarantee they will always follow the agreed rules. The authors introduce a method called Proof-Carrying Contracts where AI agents must provide a machine-checkable proof before performing actions, showing they will always follow the rules. A system called the Airlock verifies these proofs and only allows safe actions, preventing agents from breaking agreements even if they try. This approach helps build trust between parties using AI agents without needing to monitor or trust each other’s agents directly.
What this means in practice
- •For distributed system engineers: Guarantee that autonomous agents executing operations in distributed systems always comply with shared constraints using machine-checked proofs.
- •For enterprise software developers: Build secure service platforms where AI agents perform tasks only upon providing proofs that respect contractual agreements.$Commercial implications: Enables selling secure AI-driven workflow platforms that ensure contractual compliance through formal proof checking.
Authors
Carlo Ciliberto, Alessandro Rudi, Enrico Tassi
Abstract
AI agents increasingly act on behalf of people or other agents, purchasing services, exchanging information and delegating work. What an agent must respect is written in instructions, policies or agreements, but text alone cannot make it comply. It may make mistakes, be redirected by what it reads, or pursue different interests. For an economy of such agents to function, parties need agreements they can rely on without inspecting or trusting one another's agents. We introduce Proof-Carrying Contracts (PC2), a framework for making agreed constraints enforceable throughout an agent's interactions with a system. Before a requested operation can run, the agent must supply a machine-checkable proof that it preserves the agreed constraints in every case allowed by its model. An execution system called the Airlock checks the proof and controls access to the operation. The parties specify the conditions to preserve, while the agent supplies the reasoning needed to justify its decisions and remains free to adapt its strategy. This avoids having to design a separate permission policy and prove that every decision it permits is safe. We prove that the constraints hold at every instant during execution, even for an adversarial agent, and identify when this implies safety in the world. Reusable capability modules provide tools and guarantees from which contracts can be constructed. PC2 provides a foundation for an agent economy whose agreements protect both those delegating work and those carrying it out.