Lingua Universale MCP Server
Verify AI agent communication with session types and formal proofs
★ 6Apache-2.0ai-ml
Install
Config snippet generator goes here (5 client tabs)
README
<div align="center">
# Lingua Universale
**A language for verified AI agent protocols.**
[](https://pypi.org/project/cervellaswarm-lingua-universale/)
[](packages/lingua-universale/)
[](LICENSE)
[](packages/lingua-universale/)
[](https://marketplace.visualstudio.com/items?itemName=cervellaswarm.lingua-universale)
[](https://discord.gg/bvUBuejXxV)
[**Try it in your browser**](https://rafapra3008.github.io/cervellaswarm/) -- no install needed.
[**Watch AI agents live**](https://lu-debugger.fly.dev/) -- 3 agents on a verified protocol.
</div>
---
## The Problem
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.
```python
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.
---
## Install
```bash
pip install cervellaswarm-lingua-universale
```
Or try it first: [**Playground**](https://rafapra3008.github.io/cervellaswarm/) (runs in your browser via Pyodide).
---
## Write a Protocol
```
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:
```bash
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.
---
## What You Get
| 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](https://marketplace.visualstudio.com/items?itemName=cervellaswarm.lingua-universale) |
| **Interactive chat** | `lu chat` -- build protocols conversationally (English, Italian, Portuguese) |
| **Browser playground** | [Try it now](https://rafapra3008.github.io/cervellaswarm/) -- 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.
---
## CLI
```bash
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 # Inte