PluginBench
MCP Server
Active
Apache-2.0

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.

transport: stdio
Config generated by PluginBench — verify against the source before use.
~/Library/Application Support/Claude/claude_desktop_config.json
{
  "mcpServers": {
    "lu-mcp-server": {
      "command": "uvx",
      "args": [
        "lu-mcp-server"
      ]
    }
  }
}

Tools & capabilities

Tools this server exposes to the agent.

  • Protocol Compiler — Tokenizer, parser, AST builder, contract checker, and Python code generator for protocol definitions
  • Formal Verification — Proves 9 properties: always_terminates, no_deadlock, no_deletion, role_exclusive, and others via Lean 4 bridge
  • Session Checker — Runtime enforcement: validates each message against the protocol and blocks violations
  • Linter & 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 formatting
  • Interactive Chat — Conversational protocol builder (lu chat) supporting English, Italian, and Portuguese
  • CLI Tools — Commands: check, verify, run, lint, fmt, chat, demo, init, visualize, mcp-audit, repl, lsp
  • Standard Library — 20 pre-verified protocols across AI/ML, Business, Communication, Data, and Security categories
  • Visualization — 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

What is Lingua Universale?

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.

Is it free?

Yes. Lingua Universale is open-source under Apache 2.0 license. The compiler, CLI, LSP, VS Code extension, and browser playground are all free.

How do I install it?

Install via pip: `pip install cervellaswarm-lingua-universale`. Or try the browser playground at https://rafapra3008.github.io/cervellaswarm/ with no install needed.

Does it require authentication?

No. Lingua Universale is a local tool with zero external dependencies. It runs entirely on your machine.

Can I use it with Claude or other AI agents?

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.

What formal properties does it verify?

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.

<div align="center">

Lingua Universale

A language for verified AI agent protocols.

PyPI License: Apache 2.0 Zero Dependencies VS Code Discord

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

FeatureDescription
Full compilerTokenizer, parser (64 rules), AST, contract checker, Python codegen
9 verified propertiesalways_terminates, no_deadlock, no_deletion, role_exclusive, and more
20 stdlib protocolsAI/ML, Business, Communication, Data, Security -- ready to use
Linter + Formatterlu lint (10 rules) + lu fmt (zero-config, like gofmt)
LSP serverDiagnostics, hover, completion, go-to-definition, formatting
VS Code extensionInstall from Marketplace
Interactive chatlu chat -- build protocols conversationally (English, Italian, Portuguese)
Browser playgroundTry it now -- Check, Lint, Run, Chat
Lean 4 bridgeGenerate and verify mathematical proofs
REPLlu repl for interactive exploration
Project scaffoldinglu 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:

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:

PackageWhat it does
code-intelligenceAST-powered code understanding (tree-sitter, PageRank)
agent-hooksLifecycle hooks for Claude Code agents
agent-templatesAgent definition templates & team configuration
task-orchestrationDeterministic task routing & validation
spawn-workersMulti-agent process management
session-memoryPersistent session context across conversations
event-storeImmutable event logging & audit trail
quality-gatesAutomated quality checks & scoring

All Apache 2.0, Python 3.11+, tested, documented.


Contributing

We welcome contributions! See CONTRIBUTING.md for guidelines.


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

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

1
TypeScript
MIT
View repository →

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

49
Python
MIT
View repository →

Search, discover, and install 500+ AI agent skills from the SkillFlow marketplace.

1
JavaScript
MIT
View repository →

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

1
TypeScript
MIT
View repository →

All the tools you need to land your next job

View repository →
RARaily logo

Raily

Active

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

0
JavaScript
MIT
View repository →