We’ve been building CervellaSwarm for about three months — a set of Python packages for multi-agent AI systems. Today we’re sharing what we think is the most interesting part: cervellaswarm-lingua-universale, a session type system for AI agent communication.
THE PROBLEM: When multiple AI agents collaborate (a planner, a coder, a reviewer), they communicate via dictionaries and strings. No framework we could find — AutoGen, CrewAI, LangGraph, OpenAI Agents SDK, Google A2A — answers a basic question: did this agent send the right message, to the right recipient, at the right point in the protocol?
OUR APPROACH: Session types from programming language theory (Honda 1993; multiparty extension by Honda, Yoshida & Carbone, POPL 2008). We implemented them in Python so you can define a protocol, bind agents to roles, and get violations caught at runtime — not after the deployment fails.
The library also generates Lean 4 code with theorems that prove structural properties of your protocol (all senders/receivers are valid roles, no self-loops, non-empty branches). The proofs use `by decide` — decidable, machine-checkable, zero manual proof writing.
WHAT IT IS:
- Pure Python, zero dependencies, pip install and go
To our knowledge, session types haven’t been applied to AI agent communication before — we searched 242 sources across academic papers, frameworks, and protocols. If we missed prior work, we’d genuinely like to know.
lingua-universale is one of 9 CervellaSwarm packages on PyPI (the others cover code intelligence, agent hooks, task orchestration, session memory, and more). All Apache 2.0.
What we’re most curious about: do you see formal verification as relevant to multi-agent systems? We’re deciding how far to push the Lean 4 direction.
rafapra•1h ago
We’ve been building CervellaSwarm for about three months — a set of Python packages for multi-agent AI systems. Today we’re sharing what we think is the most interesting part: cervellaswarm-lingua-universale, a session type system for AI agent communication.
THE PROBLEM: When multiple AI agents collaborate (a planner, a coder, a reviewer), they communicate via dictionaries and strings. No framework we could find — AutoGen, CrewAI, LangGraph, OpenAI Agents SDK, Google A2A — answers a basic question: did this agent send the right message, to the right recipient, at the right point in the protocol?
OUR APPROACH: Session types from programming language theory (Honda 1993; multiparty extension by Honda, Yoshida & Carbone, POPL 2008). We implemented them in Python so you can define a protocol, bind agents to roles, and get violations caught at runtime — not after the deployment fails.
The library also generates Lean 4 code with theorems that prove structural properties of your protocol (all senders/receivers are valid roles, no self-loops, non-empty branches). The proofs use `by decide` — decidable, machine-checkable, zero manual proof writing.
WHAT IT IS:
- Pure Python, zero dependencies, pip install and go
- 13 modules: types, protocols, checker, DSL, monitor, Lean 4 bridge, codegen, intent parser, spec language, confidence types, trust model, error messages, agent integration
- 1,820 tests, 98% coverage
- DSL inspired by Scribble notation: `sender -> receiver : MessageKind;`
- Lean 4 verification is optional (runtime checking works without it)
Try it in 30 seconds:
pip install cervellaswarm-lingua-universale
from cervellaswarm_lingua_universale import Protocol, ProtocolStep, MessageKind, \ SessionChecker, TaskResult, TaskStatus
protocol = Protocol( name="Review", roles=("dev", "reviewer"), elements=( ProtocolStep( sender="dev", receiver="reviewer", message_kind=MessageKind.TASK_RESULT ), ), )
checker = SessionChecker(protocol) checker.send( "dev", "reviewer", TaskResult(task_id="1", status=TaskStatus.OK, summary="Done"), )
-------
Or try the interactive Colab notebook (2 min, zero setup):
https://colab.research.google.com/github/rafapra3008/cervell...
To our knowledge, session types haven’t been applied to AI agent communication before — we searched 242 sources across academic papers, frameworks, and protocols. If we missed prior work, we’d genuinely like to know.
lingua-universale is one of 9 CervellaSwarm packages on PyPI (the others cover code intelligence, agent hooks, task orchestration, session memory, and more). All Apache 2.0.
What we’re most curious about: do you see formal verification as relevant to multi-agent systems? We’re deciding how far to push the Lean 4 direction.