Alessandro Rudi

Research program

Proof Carrying Contracts (PC2)

An open protocol for enforceable agreements between AI agents acting for different people and organisations. Before an action covered by the agreement runs, the agent must supply a machine-checkable proof that it preserves the agreed constraints.

Status Paper on arXiv, October 2026; mechanization and code coming soon With Carlo Ciliberto and Enrico Tassi Groups SDA Bocconi (REAL), UCL, AI4I (PRAXIS), Inria (STAMP)

The problem

AI agents increasingly act for people and organisations: they buy services, exchange information and delegate work to other agents. What an agent must respect is written in instructions, policies or agreements, but text does not make it comply. It may make mistakes, be redirected by what it reads, or pursue interests different from those of the party it deals with.

An economy of such agents needs agreements that each party can rely on without inspecting or trusting the other party's agent.

The approach

Diagram of the Airlock. Inside it, an AI agent proposes a tool call together with a proof. A proof checker connected to the signed contract (constraints, goal, termination) accepts or rejects the pair. Accepted calls go to tool execution, which calls external services such as a database, e-mail and a calendar, and writes an execution record. Rejections return feedback to the agent; results and the current view flow back to it.
How PC2 works, Figure 1 of the paper. The agent keeps its usual loop of reasoning and tool calls inside the Airlock, but each tool call carries a proof. The proof checker, bound to the signed contract, checks the proof before the call runs: an accepted call is executed and recorded; a rejected one does not run, and the agent receives the reason.

The paper proves that the agreed constraints hold at every instant of execution, even for an adversarial agent, under stated assumptions, and identifies when this implies safety in the world. The research programme now studies whether useful requirements can be formalized faithfully, whether agents can act under them at practical cost, and what protection the resulting system provides.

What is available

Paper
Proof-Carrying Contracts: Commitments AI Agents Cannot Break. C. Ciliberto, A. Rudi, E. Tassi. arXiv:2610.28484, October 2026, 70 pages.
Website
The PC2 website: an overview of the protocol, a narrated walkthrough of a PC2 interaction and the research programme.
Code
github.com/consequential-ai/proof-carrying-contracts. The mechanization and code accompanying the paper are coming soon; a demonstration will follow.

People

Carlo Ciliberto
UCL; AI4I, Turin (PRAXIS)
Alessandro Rudi
SDA Bocconi, Milan (REAL)
Enrico Tassi
Inria (STAMP)

Take part

Seven research and engineering positions are being prepared, based in Milan (Bocconi, REAL) and Turin (AI4I, PRAXIS): see the positions. Discussion of the paper and its assumptions is welcome now; contribution instructions will come with the first implementation release.

Contact: alessandro.rudi@sdabocconi.it

Cite

@misc{ciliberto2026proofcarryingcontracts,
  title = {Proof-Carrying Contracts: Commitments {AI} Agents Cannot Break},
  author = {Carlo Ciliberto and Alessandro Rudi and Enrico Tassi},
  year = {2026},
  eprint = {2610.28484},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/pdf/2610.28484}
}