Lingua Universale MCP Server

io.github.rafapra3008Published by GitHub account rafapra3008v0.1.1Updated Oct 24, 2026

Verify AI agent communication with session types and formal proofs

VerifiedSTDIODesktop onlyDeveloper Tools AI & ML

Server details

Identifier: io.github.rafapra3008/lu-mcp-server
Transport: STDIO
Runtime: Desktop only
Trust: Verified
Published: Sep 16, 2026

Security note

MCP servers receive tool arguments from a conversation and may perform external actions. Review what a server can do before you enable it, and give it only the access it needs.

The registry verified the GitHub account rafapra3008 for this listing. That does not show the account is the product's maker.

SourceWeft's checks cover whether the listing is complete and the endpoint answered; they do not review the server's code or what its tools do.

Add a badge to your README

Show readers this MCP server is listed on SourceWeft. The badge links to this page.

[![Listed on SourceWeft](https://sourceweft.com/badge/mcp/io.github.rafapra3008%2Flu-mcp-server.svg)](https://sourceweft.com/mcp/io.github.rafapra3008%2Flu-mcp-server?utm_source=readme&utm_medium=badge)

Overview

AI-generated overview

A local MCP server for Lingua Universale, a session-type tool that lets an assistant define, verify and enforce protocols for AI agent conversations.

What you can do: Define agent protocols with roles, message order and choice branches, then check and formally verify properties such as termination, deadlock freedom and role participation. Lint, format and visualize protocols, and scaffold projects from verified templates. Run protocols and audit MCP server protocol manifests. Generate Lean 4 proofs and Python code from protocol sources.
When to use it: Useful when you are building multi-agent systems and want the assistant to write, verify or debug the communication protocol between agents, or to add protocol verification to a CI pipeline.
Requirements: Runs as a local process over stdio, launched with uvx from the lu-mcp-server PyPI package, so a Python environment with uv is needed. No authentication, environment variables or headers are declared.

Before you install

The README's install instructions reference a different package name than the manifest, so confirm which package you are installing. Protocol verification and code generation act on your own protocol files; review generated code before running it.

Installation

In SourceWeft

Open Lingua Universale MCP Server in the dashboard and add it to a workspace.
Enable the server for the chats that should use its tools.

Desktop only via STDIO. STDIO servers start a local process, so they need the SourceWeft desktop host.

Other MCP clients

Follow the launch instructions in the repository.

README

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.

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 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

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

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

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:

  [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.

  [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

bash

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

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:

yaml

# .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/

# .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 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.

Lingua Universale -- Verified protocols for AI agents.

Source: README.md at commit e1aea16

Tools

SourceWeft has not started this package in its sandbox yet, so its tools are not known.

Version history

v0.1.1LatestSep 16, 2026

Score

50% of the applicable checks met

How complete this listing is, computed from the registry entry, the endpoint and public sources. Not a rating of the server and not a statement that it is safe or working today: reachability is a dated check, and no installs or reviews go into the score.

Reached in the last 30 days25 pts
Keep the endpoint answering the MCP handshake; SourceWeft probes it every 30 days.
Auth declared10 pts
Declare the credential headers in the registry entry, or keep the endpoint answering the probe so its auth can be classified.
Tools listed15 pts
Answer tools/list without a credential, or ship a package that starts in a sandbox without one.
DescriptionRequired15 pts
Logo10 pts
Documentation15 pts
License10 pts