Lingua Universale MCP Server

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 orderreview = 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"))  # OKchecker.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

Zero external dependencies. Pure Python stdlib.

CLI

lu check file.lu          # Parse and compilelu verify file.lu         # Formal property verificationlu run file.lu            # Executelu lint file.lu           # 10 style and correctness ruleslu fmt file.lu            # Zero-config auto-formatterlu chat --lang en         # Build a protocol conversationallylu demo --lang it         # See the La Nonna demolu init --template NAME   # Scaffold from stdlib templateslu visualize file.lu      # Generate Mermaid sequence diagramlu mcp-audit --manifest t.json  # Audit MCP server protocolslu repl                   # Interactive REPLlu lsp                    # Start LSP server

CI Integration

Add protocol verification to your GitHub Actions workflow:

# .github/workflows/lu-check.ymlon:  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:

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.