Lingua Universale MCP Server MCP Server
io.github.rafapra3008/lu-mcp-server
Type checker for AI agent conversations—define protocols, prove correctness, enforce at runtime.
What is the Lingua Universale MCP Server MCP server?
Lingua Universale is a language and type checker for verified AI agent protocols. It lets you define communication rules between agents, formally proves the protocol is correct (no deadlocks, wrong message order, or missing steps), and enforces those rules at runtime. Built on multiparty session types, it generates Python code and Lean 4 proofs to guarantee your agents follow the protocol.
Lingua Universale prevents AI agents from miscommunicating by treating agent protocols as types. You write a protocol definition (who sends what, to whom, in what order), LU verifies 9 formal properties mathematically, and the runtime blocks any violation. It includes a full compiler, CLI tools (check, verify, lint, format), LSP server, VS Code extension, 20 stdlib protocols, and a browser playground—all with zero external dependencies.
How to install Lingua Universale MCP Server
Copy-paste configuration for popular MCP clients.
Tools & capabilities
Tools this server exposes to the agent.
Protocol Compiler— Tokenizer, parser, AST builder, contract checker, and Python code generator for protocol definitionsFormal Verification— Proves 9 properties: always_terminates, no_deadlock, no_deletion, role_exclusive, and others via Lean 4 bridgeSession Checker— Runtime enforcement: validates each message against the protocol and blocks violationsLinter & Formatter— 10 style/correctness rules (lu lint) and zero-config auto-formatter (lu fmt)LSP Server— Language Server Protocol with diagnostics, hover, completion, go-to-definition, and formattingInteractive Chat— Conversational protocol builder (lu chat) supporting English, Italian, and PortugueseCLI Tools— Commands: check, verify, run, lint, fmt, chat, demo, init, visualize, mcp-audit, repl, lspStandard Library— 20 pre-verified protocols across AI/ML, Business, Communication, Data, and Security categoriesVisualization— Generate Mermaid sequence diagrams from protocol definitions
Use cases
- Define and verify multi-agent orchestration protocols to prevent deadlocks and message-ordering bugs
- Enforce strict communication rules between Claude API agents at runtime with formal guarantees
- Audit MCP server manifests for protocol correctness using lu mcp-audit
- Build conversational AI workflows (RAG pipelines, review cycles, delegation chains) with mathematical proof of correctness
- Integrate protocol verification into CI/CD pipelines to catch communication violations before production
Lingua Universale MCP Server MCP server FAQ
A type checker and runtime enforcer for AI agent communication protocols. You define the protocol, LU proves it's mathematically correct (no deadlocks, wrong order, missing steps), and the runtime blocks violations.
Yes. Lingua Universale is open-source under Apache 2.0 license. The compiler, CLI, LSP, VS Code extension, and browser playground are all free.
Install via pip: `pip install cervellaswarm-lingua-universale`. Or try the browser playground at https://rafapra3008.github.io/cervellaswarm/ with no install needed.
No. Lingua Universale is a local tool with zero external dependencies. It runs entirely on your machine.
Yes. You define a protocol in LU, generate Python code, and use the SessionChecker to validate messages from your agents. The LU Debugger demo shows 3 Claude API agents running on a verified protocol.
9 properties including: always_terminates, no_deadlock, no_deletion, role_exclusive, and others. Each is proved mathematically via Lean 4, not tested.
README (reference)
Source of truth, from the repository.
Lingua Universale
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.
</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.
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
pip install cervellaswarm-lingua-universale
Or try it first: Playground (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:
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 |
| 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 |
Zero external dependencies. Pure Python stdlib.
CLI
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 server
CI Integration
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.
How It Works
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.
Examples
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.
More from CervellaSwarm
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.11+, tested, documented.
Contributing
We welcome contributions! See CONTRIBUTING.md for guidelines.
- Bug reports: GitHub Issues
- Security: See SECURITY.md for responsible disclosure
License
Apache License 2.0 -- see LICENSE.
Copyright 2025-2026 CervellaSwarm Contributors.
<div align="center">
Lingua Universale -- Verified protocols for AI agents.
Playground | LU Debugger | PyPI | VS Code | Blog | Colab Demo
</div>Related MCP servers

io.github.rafavecchi/grantd
Grantd MCP server: let your AI agent act on a user's behalf across third-party APIs via OAuth.

Credit Optimizer v5 for Manus AI
Save 30-75% on Manus AI credits via intelligent model routing and smart task detection.

io.github.rafsilva85/skillflow
Search, discover, and install 500+ AI agent skills from the SkillFlow marketplace.

Pipes Claude Code session output into Claude Chat — no more copy-paste between tools

Raily
Raily personal-agent MCP with scoped reads and approved actions.
