A protocol-first approach to LLM agents
Most agent systems are wired together locally, one call at a time, and you find out how the pieces interact by running them. ZipperGen asks you to write the protocol first: who talks to whom, who performs each action, and who owns each decision. The local program each participant runs is derived from that, not written by hand.
What follows from that
- The global workflow is the source of truth, and it is readable.
- A participant's program mentions only what concerns it, so it cannot wait for a message the decider chose not to send.
- Human approval and side effects are explicit, not buried in a callback.
- For well-formed workflows, the coordination layer is deadlock-free by construction rather than by testing.
Where it comes from
The projection is based on Message Sequence Charts and choreographic programming, adapted to LLM agents, tool calls and human approval. The core theorem is machine-checked in Lean 4. The code, the examples and the tests are on GitHub.