lu-mcp-server

lu-mcp-server

Verify AI agent communication with session types and formal proofs. 4 tools: parse protocols, verify messages, check safety properties, browse 20 stdlib templates.

Category
Visit Server

README

<div align="center">

Lingua Universale

A language for verified AI agent protocols.

PyPI Tests License: Apache 2.0 Zero Dependencies VS Code

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

36 modules. 3867 tests. 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 repl                   # Interactive REPL
lu lsp                    # Start LSP server

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:

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.


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>

Recommended Servers

playwright-mcp

playwright-mcp

A Model Context Protocol server that enables LLMs to interact with web pages through structured accessibility snapshots without requiring vision models or screenshots.

Official
Featured
TypeScript
Magic Component Platform (MCP)

Magic Component Platform (MCP)

An AI-powered tool that generates modern UI components from natural language descriptions, integrating with popular IDEs to streamline UI development workflow.

Official
Featured
Local
TypeScript
Audiense Insights MCP Server

Audiense Insights MCP Server

Enables interaction with Audiense Insights accounts via the Model Context Protocol, facilitating the extraction and analysis of marketing insights and audience data including demographics, behavior, and influencer engagement.

Official
Featured
Local
TypeScript
VeyraX MCP

VeyraX MCP

Single MCP tool to connect all your favorite tools: Gmail, Calendar and 40 more.

Official
Featured
Local
graphlit-mcp-server

graphlit-mcp-server

The Model Context Protocol (MCP) Server enables integration between MCP clients and the Graphlit service. Ingest anything from Slack to Gmail to podcast feeds, in addition to web crawling, into a Graphlit project - and then retrieve relevant contents from the MCP client.

Official
Featured
TypeScript
Kagi MCP Server

Kagi MCP Server

An MCP server that integrates Kagi search capabilities with Claude AI, enabling Claude to perform real-time web searches when answering questions that require up-to-date information.

Official
Featured
Python
E2B

E2B

Using MCP to run code via e2b.

Official
Featured
Neon Database

Neon Database

MCP server for interacting with Neon Management API and databases

Official
Featured
Exa Search

Exa Search

A Model Context Protocol (MCP) server lets AI assistants like Claude use the Exa AI Search API for web searches. This setup allows AI models to get real-time web information in a safe and controlled way.

Official
Featured
Qdrant Server

Qdrant Server

This repository is an example of how to create a MCP server for Qdrant, a vector search engine.

Official
Featured