Verify AI agent communication with session types and formal proofs
A language for verified AI agent protocols.
Try it in your browser -- no install needed. Watch AI agents live -- 3 agents on a verified protocol.
Your AI agents talk to each other, but nothing guarantees they follow the rules. Wrong sender, wrong message order, missing steps -- and you only find out in production.
Lingua Universale (LU) is a type checker for AI agent conversations. You define the protocol, LU proves it's correct, and the runtime enforces it.
from cervellaswarm_lingua_universale import Protocol, ProtocolStep, MessageKind, SessionChecker, TaskRequest
# Define: who sends what, to whom, in what order
review = Protocol(name="Review", roles=("dev", "reviewer"), elements=(
ProtocolStep(sender="dev", receiver="reviewer", message_kind=MessageKind.TASK_REQUEST),
ProtocolStep(sender="reviewer", receiver="dev", message_kind=MessageKind.TASK_RESULT),
))
checker = SessionChecker(review)
checker.send("dev", "reviewer", TaskRequest(task_id="1", description="Review auth")) # OK
checker.send("dev", "reviewer", TaskRequest(task_id="2", description="Oops")) # ProtocolViolation!
# ^^^ wrong turn: reviewer must send next
The protocol says reviewer goes next. The runtime blocks it. Not because you trust the code -- because the session type makes it impossible.
pip install cervellaswarm-lingua-universale
Or try it first: Playground (runs in your browser via Pyodide).
protocol DelegateTask:
roles: supervisor, worker, validator
supervisor asks worker to execute analysis
worker returns result to supervisor
supervisor asks validator to verify result
when validator decides:
pass:
validator returns approval to supervisor
fail:
validator sends feedback to supervisor
properties:
always terminates
no deadlock
no deletion
all roles participate
Then verify it:
lu verify delegate_task.lu
[1/4] always_terminates ... PROVED
[2/4] no_deadlock ... PROVED
[3/4] no_deletion ... PROVED
[4/4] all_roles_participate ... PROVED
All 4 properties PASSED.
Mathematical proof. Not a test that passes today and fails tomorrow.
| Feature | Description |
|---|---|
| Full compiler | Tokenizer, parser (64 rules), AST, contract checker, Python codegen |
| 9 verified properties | always_terminates, no_deadlock, no_deletion, role_exclusive, and more |
| 20 stdlib protocols | AI/ML, Business, Communication, Data, Security -- ready to use |
| Linter + Formatter | lu lint (10 rules) + lu fmt (zero-config, like gofmt) |
| LSP server | Diagnostics, hover, completion, go-to-definition, formatting |
| VS Code extension | Install from Marketplace |
| Interactive chat | lu chat -- build protocols conversationally (English, Italian, Portuguese) |
| Browser playground | Try it now -- Check, Lint, Run, Chat |
| Lean 4 bridge | Generate and verify mathematical proofs |
| REPL | lu repl for interactive exploration |
| Project scaffolding | lu init --template rag_pipeline from 20 verified templates |
36 modules. 3920 tests. Zero external dependencies. Pure Python stdlib.
lu check file.lu # Parse and compile
lu verify file.lu # Formal property verification
lu run file.lu # Execute
lu lint file.lu # 10 style and correctness rules
lu fmt file.lu # Zero-config auto-formatter
lu chat --lang en # Build a protocol conversationally
lu demo --lang it # See the La Nonna demo
lu init --template NAME # Scaffold from stdlib templates
lu mcp-audit --manifest t.json # Audit MCP server protocols
lu repl # Interactive REPL
lu lsp # Start LSP server
Add protocol verification to your GitHub Actions workflow:
# .github/workflows/lu-check.yml
on:
push:
paths: ["**/*.lu"]
jobs:
lu-check:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: actions/setup-python@v6
with:
python-version: "3.11"
- run: pip install cervellaswarm-lingua-universale
- run: lu lint protocols/
- run: lu verify protocols/
Exit code is non-zero on violations -- works with any CI system.
LU is built on multiparty session types (Honda, Yoshida, Carbone -- POPL 2008). Session types describe communication protocols as types: if two processes follow the same session type, they cannot deadlock, messages cannot arrive in the wrong order, and the conversation always terminates.
The pipeline:
.lu source → Tokenizer → Parser → AST → Spec Checker → Lean 4 Proofs → Python Codegen
↓
PROVED or VIOLATED
LU doesn't replace your AI agent framework. It makes it safe. Like TypeScript for JavaScript -- you keep your tools, you add guarantees.
LU Debugger -- Live web app: 3 AI agents (Customer, Warehouse, Payment) communicate on a verified OrderProcessing protocol. Click "Break" to see a protocol violation blocked in real time. Source code.
See the examples/ directory:
Or try the interactive Colab notebook -- 2 minutes, zero setup.
Lingua Universale is the core project by CervellaSwarm. We also publish these Python packages:
| Package | What it does |
|---|---|
| code-intelligence | AST-powered code understanding (tree-sitter, PageRank) |
| agent-hooks | Lifecycle hooks for Claude Code agents |
| agent-templates | Agent definition templates & team configuration |
| task-orchestration | Deterministic task routing & validation |
| spawn-workers | Multi-agent process management |
| session-memory | Persistent session context across conversations |
| event-store | Immutable event logging & audit trail |
| quality-gates | Automated quality checks & scoring |
All Apache 2.0, Python 3.10+, tested, documented.
We welcome contributions! See CONTRIBUTING.md for guidelines.
Apache License 2.0 -- see LICENSE.
Copyright 2025-2026 CervellaSwarm Contributors.
Lingua Universale -- Verified protocols for AI agents.
Playground | LU Debugger | PyPI | VS Code | Blog | Colab Demo
Source-derived launch command. Check the maintainer’s required arguments and credentials before running:
uvx lu-mcp-serverMerge this template into ~/Library/Application Support/Claude/claude_desktop_config.json. Keep existing servers. Add any arguments, credentials, and permissions required by the maintainer; this template has not been install-tested.
{
"mcpServers": {
"io-github-rafapra3008-lu-mcp-server": {
"command": "uvx",
"args": [
"lu-mcp-server"
]
}
}
}Restart Claude Desktop completely for changes to take effect. Confirm the server appears connected in the client’s tool list, then try a read-only example from its documentation.
Claude Desktop setup referenceLingua Universale MCP Server works with any MCP-compatible client. Copy the config snippet from the Configuration section above and add it to the file shown for your client, then restart the application.
~/Library/Application Support/Claude/claude_desktop_config.jsonRestart Claude Desktop completely for changes to take effect.~/.cursor/mcp.jsonRestart Cursor for changes to take effect..vscode/mcp.jsonReload VS Code window for changes to take effect.~/.codeium/windsurf/mcp_config.jsonRestart Windsurf for changes to take effect..mcp.jsonSave at the project root, then start Claude Code in that project and review the MCP server approval prompt. Keep real credentials out of shared files.