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 nextThe 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-universaleOr 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 |
37 modules. 3979 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 visualize file.lu # Generate Mermaid sequence diagram
lu mcp-audit --manifest t.json # Audit MCP server protocols
lu repl # Interactive REPL
lu lsp # Start LSP serverAdd 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:
- Agent Orchestration -- 3 AI agents with nested choice, 8/8 properties proved
- Live Runner -- Real Claude API agents on a verified protocol
- Standard Library -- 20 verified protocols across 5 categories
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.
- Bug reports: GitHub Issues
- Security: See SECURITY.md for responsible disclosure
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