How PC2 works

A principal is the person or organisation an agent represents. Consider a traveller's agent commissioning a provider's agent to arrange a trip. The traveller specifies a budget and rules for disclosing documents. The provider agrees what it will deliver and what evidence establishes completion.

The parties express the agreement as a formal contract. It describes the relevant resources and their initial state, the constraints that must remain satisfied, and the goal that defines completion. A paid interaction also specifies its payment arrangement and the conditions for expiry or refund.

Contract assistants can draft candidate terms, explain them in ordinary language and generate examples that reveal ambiguity or unintended permissions. These steps help the principals review what the formal contract actually permits before approving it. Enforcement applies to the signed terms; a mismatch with the intended requirement remains possible.

The Airlock is the controlled execution environment in PC2's reference design. It maintains the contractual state and mediates the executing agent's access to the governed resources. Before signing, both principals check its remote attestation: evidence that it runs the agreed reference build.

For each proposed tool call, the system constructs the statement that must be proved under the contract and current state. The proof must establish that every outcome covered by the tool's declared model preserves the required constraints.

PC2's reference research uses Lean, a proof assistant that checks formal proofs against precise definitions and logical rules. Models and automated methods can construct candidate proofs; the checker validates the final argument independently of how it was generated.

Without an accepted proof, the governed tool call does not execute. The agent can revise its plan, seek further evidence or stop. A failed attempt may reflect the limits or cost of proof search even when the proposed action satisfies the contract.

Each executed call updates the recorded state. For example, a new booking must be considered together with money already committed to the trip. The guarantee is relative to the signed contract and its trusted base: the proof checker and obligation compiler, the Airlock, tool models and implementations, and the attestation and payment infrastructure. Expert verdicts, when used, are also assumptions of the reasoning.

A provider may assign the visa part of a travel task to a sub-agent acting for another principal. The subcontract defines that subtask, the resources available to the sub-agent and the conditions under which it may act.

PC2 treats delegation as a governed action. Before creating a subcontract, the contractor must supply a proof that the proposed child contract, considered together with its outstanding delegations, preserves the parent contract's constraints and resource limits.

In the travel example, the visa service receives the authority and access assigned to its subtask. Documents governed by the contract remain in controlled custody and are accessed through the permitted interfaces. The parent agreement continues to constrain the overall task as work passes between agents.

The proposed composition guarantee applies within a contract tree. Aggregate obligations and interference across separate contract trees remain open research questions.

Completion is governed by the contract, whether or not work has been delegated. The executing agent uses recorded actions, delegation certificates and any agreed expert verdicts to prove that the goal has been reached. Where payment is involved, settlement requires the corresponding checked proof. Expiry and refund conditions follow the contract and the selected payment mechanism.