pith. machine review for the scientific record. sign in

arxiv: 2605.03143 · v1 · submitted 2026-05-04 · 💻 cs.PL · cs.AI· cs.DC

Recognition: unknown

Pact: A Choreographic Language for Agentic Ecosystems

Kiran Gopinathan , Jack Feser , Michelangelo Naim , Zenna Tavares , Eli Bingham
Authors on Pith no claims yet

Pith reviewed 2026-05-08 01:25 UTC · model grok-4.3

classification 💻 cs.PL cs.AIcs.DC
keywords choreographic programminggame theoryagentic systemsprotocol designformal gamesdecision policiesmulti-party coordination
0
0 comments X

The pith

Pact maps every choreographic protocol to a formal game so designers can solve for self-interested agents' decisions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Pact as an extension of choreographic programming that adds operations for agent choices and preferences taken from game theory. This extension produces a direct mapping from each protocol to a formal game. The mapping lets protocol designers apply game-theoretic reasoning to find decision policies that agents would follow based on their preferences. A reader would care because standard choreographic methods assume cooperative participants, yet real agentic systems involve autonomous actors that may act in self-interest when handling private data or interacting with untrusted parties. The paper also supplies a preliminary bounded-rational solver that computes such policies and tests the approach on multi-party coordination examples.

Core claim

Pact is a choreographic language extended with operations to describe agent choices and preferences drawing from game theory. Every Pact protocol maps to a formal game, allowing protocol designers to reason about game-theoretic properties of their protocols such as solving for decision policies. The work includes a preliminary implementation of a bounded-rational solver that computes decision policies over Pact protocols and reports findings from applying the language to multi-party coordination with self-interested agentic participants.

What carries the argument

The mapping from Pact protocols to formal games, which transfers game-theoretic analysis tools into the choreographic setting while retaining protocol structure.

If this is right

  • Protocol designers gain the ability to compute decision policies for agents using the bounded-rational solver.
  • Game-theoretic properties such as equilibria can be analyzed directly on choreographic protocols.
  • Multi-party coordination becomes possible in settings where agents hold private information and interact with untrusted counterparts.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same mapping could support larger game solvers beyond the preliminary bounded-rational implementation described.
  • Pact-style protocols might be tested in domains such as automated negotiation where self-interest is explicit.
  • The interaction between choreographic correctness and game equilibria could be examined as a separate verification step.

Load-bearing premise

That adding operations for agent choices and preferences to choreographic programming preserves its correct-by-construction guarantees and that the mapping to formal games faithfully captures self-interest without inconsistencies.

What would settle it

Implementing agents that follow the decision policies computed by the Pact solver and checking whether those policies produce the same outcomes as rational play in the corresponding formal game under a multi-party simulation.

Figures

Figures reproduced from arXiv: 2605.03143 by Eli Bingham, Jack Feser, Kiran Gopinathan, Michelangelo Naim, Zenna Tavares.

Figure 1
Figure 1. Figure 1: A choreographic bookseller protocol (left) and its endpoint projections for buyer (middle) and seller view at source ↗
Figure 2
Figure 2. Figure 2: Pact encoding of the full buyer seller protocol, with explicit agent choices, prefer￾ences and priors over the world. Putting it all together view at source ↗
Figure 3
Figure 3. Figure 3: Recursive theory-of-mind structure for the buyer-seller protocol. Each agent maintains a generative view at source ↗
Figure 4
Figure 4. Figure 4: Buyer Theory of Mind Once the model is constructed, we can then run infer￾ence over it to obtain a decision policy that can be used to run the protocol — a mapping from observed prices to a probability of accepting. When we run inference over this protocol, we are able to recreate aspects of the phenomenon of the marketplace for lemons [3]: with a depth 0 reasoning, the buyer naively assumes that high pric… view at source ↗
read the original abstract

Recent advances in large language models have led to the rise of software systems (i.e. agents) that execute with increasing autonomy on behalf of users in open, multi-party settings, interacting with untrusted counterparts and managing private information. Choreographic programming offers correct-by-construction protocol-design for such settings, but assumes cooperative participants -- it has no notion of agent self-interest, that is, why an agent will follow a protocol. In this talk we introduce Pact, a choreographic language extended with operations to describe agent choices and preferences, drawing from the rich literature of game theory. Every Pact protocol maps to a formal game, allowing protocol designers to reason about game-theoretic properties of their protocols, such as solving for decision policies. We present Pact's design and a preliminary implementation -- a bounded-rational solver that computes decision policies over Pact protocols -- and findings from applying this language to multi-party coordination with self-interested agentic participants.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces Pact, an extension of choreographic programming that adds game-theoretic operations for modeling agent choices and preferences in multi-party settings with self-interested participants. It claims that every Pact protocol maps to a formal game, enabling reasoning about properties such as decision policies, and presents a preliminary implementation consisting of a bounded-rational solver along with applications to multi-party coordination.

Significance. If the claimed mapping to formal games can be established rigorously while preserving correct-by-construction guarantees, the work could meaningfully connect choreographic programming with game theory for designing protocols in autonomous agent ecosystems. This would allow protocol designers to incorporate self-interest and solve for equilibria, addressing a gap in existing choreographic approaches that assume cooperation.

major comments (2)
  1. [Pact design and mapping] The central claim that every Pact protocol maps to a formal game (allowing solution for decision policies) lacks any formal semantics, typing rules, or explicit definition of the mapping. Without these, it is impossible to verify that the extension preserves the correct-by-construction properties of choreographies or that the game faithfully captures self-interest without inconsistencies.
  2. [Implementation and findings] The preliminary implementation section describes a bounded-rational solver at a high level but provides no evaluation results, benchmarks, error analysis, or case studies with concrete protocols. This undermines assessment of whether the solver can practically compute decision policies over non-trivial Pact protocols.
minor comments (1)
  1. The abstract and introduction would benefit from a clearer separation between the language design contribution and the solver implementation, including explicit statements of what is proven versus what is preliminary.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback, which highlights important areas for strengthening the presentation of Pact. We address each major comment below and indicate the revisions we will incorporate.

read point-by-point responses

  1. Referee: [Pact design and mapping] The central claim that every Pact protocol maps to a formal game (allowing solution for decision policies) lacks any formal semantics, typing rules, or explicit definition of the mapping. Without these, it is impossible to verify that the extension preserves the correct-by-construction properties of choreographies or that the game faithfully captures self-interest without inconsistencies.

    Authors: We agree that the manuscript presents the mapping from Pact protocols to formal games at a conceptual level without a complete formal semantics or typing rules. This reflects the preliminary nature of the work, which prioritizes introducing the language design and its game-theoretic extension over a full metatheoretic development. The high-level mapping is illustrated through examples that show how agent choices and preferences are encoded as game elements, but we acknowledge this is insufficient for rigorous verification. In the revised manuscript we will add an explicit definition of the mapping, a sketch of the extended semantics that preserves correct-by-construction guarantees by treating game-theoretic operations as additional choreography constructs, and a clarification of how utilities are assigned to capture self-interest without introducing inconsistencies. We will also note that a full proof of preservation is left for future work. revision: yes

  2. Referee: [Implementation and findings] The preliminary implementation section describes a bounded-rational solver at a high level but provides no evaluation results, benchmarks, error analysis, or case studies with concrete protocols. This undermines assessment of whether the solver can practically compute decision policies over non-trivial Pact protocols.

    Authors: We concur that the current description of the bounded-rational solver is high-level and lacks concrete evaluation data. The manuscript emphasizes the language and the solver's conceptual role rather than empirical validation, consistent with its positioning as an initial introduction. To address this, the revised version will include case studies with concrete multi-party protocols, performance benchmarks on protocols of varying size, and an error analysis of the solver's approximations. These additions will demonstrate the practical feasibility of computing decision policies while clearly delineating the preliminary scope of the implementation. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected in derivation chain

full rationale

The paper introduces Pact as a language extension of choreographic programming with game-theoretic operations for choices and preferences, together with a claimed mapping from every Pact protocol to a formal game. No load-bearing step reduces by construction to its own inputs: the mapping is presented as a design contribution rather than a fitted parameter or self-defined quantity, the correct-by-construction preservation is stated as an assumption drawn from prior choreographic programming literature (external to this work), and no self-citation chain or uniqueness theorem imported from the authors' prior work is invoked to force the central result. The preliminary bounded-rational solver is described as an implementation artifact, not as a prediction that is statistically forced by the same data used to define the language. The derivation therefore remains self-contained as a language-design proposal whose core claims do not collapse into re-labeling or re-fitting of the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The abstract provides no details on free parameters, axioms, or invented entities; assessment is limited to the high-level description of the language extension.

pith-pipeline@v0.9.0 · 5467 in / 1027 out tokens · 48713 ms · 2026-05-08T01:25:19.490247+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 13 canonical work pages · 4 internal anchors

  1. [1]

    [n. d.]. Agents Rule of Two: A Practical Approach to AI Agent Security. https://ai.meta.com/blog/practical-ai-agent- security/

  2. [2]

    Varshney

    2026. Multi-Agent AI Systems Need Transparency.Nature Machine Intelligence8, 1 (Jan. 2026), 1–1. doi:10.1038/s42256- 026-01183-2

    work page doi:10.1038/s42256- 2026

  3. [3]

    George A. Akerlof. 1970. The Market for "Lemons": Quality Uncertainty and the Market Mechanism.The Quarterly Journal of Economics84, 3 (Aug. 1970), 488–500

    1970

  4. [4]

    2024.Effectful: Algebraic Effects for Python

    Basis Research Institute. 2024.Effectful: Algebraic Effects for Python. https://github.com/BasisResearch/effectful https://github.com/BasisResearch/effectful

    2024

  5. [5]

    Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, and Joseph P. Near. 2025. Efficient, Portable, Census-Polymorphic Choreographic Programming.Proc. ACM Program. Lang.9, PLDI (June 2025), 193:1143–193:1166. doi:10.1145/3729296

    work page doi:10.1145/3729296 2025

  6. [6]

    Noah Bertram, Alex Levinson, and Justin Hsu. 2023. Cutting the Cake: A Language for Fair Division.Proceedings of the ACM on Programming Languages7, PLDI (June 2023), 1779–1800. arXiv:2304.04642 [cs] doi:10.1145/3591293 Comment: 31 pages, 15 figures, PLDI 2023

    work page doi:10.1145/3591293 2023

  7. [7]

    Chi-Min Chan, Weize Chen, Yusheng Su, Jianxuan Yu, Wei Xue, Shanghang Zhang, Jie Fu, and Zhiyuan Liu. 2023. ChatEval: Towards Better LLM-based Evaluators through Multi-Agent Debate. arXiv:2308.07201 [cs] doi:10.48550/ arXiv.2308.07201

    work page internal anchor Pith review arXiv 2023

  8. [8]

    Tenenbaum, and Jonathan Ragan-Kelley

    Kartik Chandra, Tony Chen, Joshua B. Tenenbaum, and Jonathan Ragan-Kelley. 2025. A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning.Proc. ACM Program. Lang.9, OOPSLA2 (2025). doi:10.1145/ 3763078

    2025

  9. [9]

    Dave De Jonge and Dongmo Zhang. 2021. GDL as a Unifying Domain Description Language for Declarative Automated Negotiation.Autonomous Agents and Multi-Agent Systems35, 1 (April 2021), 13. doi:10.1007/s10458-020-09491-6

    work page doi:10.1007/s10458-020-09491-6 2021

  10. [10]

    Edoardo Debenedetti, Ilia Shumailov, Tianqi Fan, Jamie Hayes, Nicholas Carlini, Daniel Fabian, Christoph Kern, Chongyang Shi, Andreas Terzis, and Florian Tramèr. 2025. Defeating prompt injections by design.arXiv preprint arXiv:2503.18813(2025)

    work page internal anchor Pith review arXiv 2025

  11. [11]

    Edoardo Debenedetti, Jie Zhang, Mislav Balunovic, Luca Beurer-Kellner, Marc Fischer, and Florian Tramèr. 2024. AgentDojo: A Dynamic Environment to Evaluate Prompt Injection Attacks and Defenses for LLM Agents. InAdvances in Neural Information Processing Systems, A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang (Eds.), Vol....

    work page doi:10.52202/079017-2636 2024

  12. [12]

    Yilun Du, Shuang Li, Antonio Torralba, Joshua B Tenenbaum, and Igor Mordatch. 2023. Improving factuality and reasoning in language models through multiagent debate.arXiv preprint arXiv:2305.14325(2023)

    work page internal anchor Pith review arXiv 2023

  13. [13]

    Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. 2024. Choral: Object-oriented Choreographic Programming. ACM Transactions on Programming Languages and Systems46, 1 (March 2024), 1–59. doi:10.1145/3632398

    work page doi:10.1145/3632398 2024

  14. [14]

    Sirui Hong, Mingchen Zhuge, Jiaqi Chen, Xiawu Zheng, Yuheng Cheng, Ceyao Zhang, Jinlin Wang, Zili Wang, Steven Ka Shing Yau, Zijuan Lin, Liyang Zhou, Chenyu Ran, Lingfeng Xiao, Chenglin Wu, and Jürgen Schmidhuber. 2024. MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework. arXiv:2308.00352 [cs] doi:10.48550/arXiv. 2308.00352

    work page internal anchor Pith review doi:10.48550/arxiv 2024

  15. [15]

    Samaneh Hoseindoost, Afsaneh Fatemi, and Bahman Zamani. 2024. An Executable Domain-Specific Modeling Language for Simulating Organizational Auction-Based Coordination Strategies for Crisis Response.Simulation Modelling Practice and Theory131 (Feb. 2024), 102880. doi:10.1016/j.simpat.2023.102880 , Vol. 1, No. 1, Article . Publication date: May 2026. 8 Gopi...

    work page doi:10.1016/j.simpat.2023.102880 2024

  16. [16]

    Yupei Liu, Yuqi Jia, Runpeng Geng, Jinyuan Jia, and Neil Zhenqiang Gong. 2024. Formalizing and Benchmarking Prompt Injection Attacks and Defenses. In33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 1831–1847. https://www.usenix.org/conference/usenixsecurity24/presentation/liu-yupei

    2024

  17. [17]

    Nathaniel Love, Timothy Hinrichs, David Haley, Eric Schkufza, Michael Genesereth, and Serra Mall. [n. d.]. General Game Playing: Game Description Language Specification. ([n. d.])

  18. [18]

    2023.Introduction to Choreographies

    Fabrizio Montesi. 2023.Introduction to Choreographies. Cambridge University Press, Cambridge. doi:10.1017/ 9781108981491

    2023

  19. [19]

    Abhiroop Sarkar and Alejandro Russo. 2024. HasTEE+ : Confidential Cloud Computing and Analytics with Haskell. arXiv:2401.08901 [cs] doi:10.48550/arXiv.2401.08901

    work page doi:10.48550/arxiv.2401.08901 2024

  20. [20]

    Gan Shen, Shun Kashiwa, and Lindsey Kuper. 2023. HasChor: Functional Choreographic Programming for All (Functional Pearl).Proc. ACM Program. Lang.7, ICFP (Aug. 2023), 207:541–207:565. doi:10.1145/3607849

    work page doi:10.1145/3607849 2023

  21. [21]

    Gan Shen and Lindsey Kuper. 2024. Toward Verified Library-Level Choreographic Programming with Algebraic Effects. InProceedings of the International Conference on Choreographic Programming (CP). University of California, Santa Cruz, USA. Pre-print

    2024

  22. [22]

    2025.Choreographies for Secure Computation

    Manuel Veiga. 2025.Choreographies for Secure Computation. Ph. D. Dissertation. University of Porto

    2025

  23. [23]

    Zhicheng Yang, Li Peihang, Wuqiang Zheng, Zhiyang Dou, Minghao Guo, Benjamin Tod Jones, and Wojciech Matusik

  24. [24]

    MIND: Market Interpretation DSL for Unified Market Design and Simulation. (Oct. 2025). Received 30 March 2026 , Vol. 1, No. 1, Article . Publication date: May 2026

    2025