Lingua Universale

MCP serverAI & models

Verify AI agent communication with session types and formal proofs

Unavailable. This server has no hosted endpoint yet, so ahel can't serve it.

Connect ahel once, and every AI you use reads what you have installed.

From the project's README

As published by rafapra3008/cervellaswarm in README.md.

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.


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.


Lingua Universale -- Verified protocols for AI agents.

Playground | LU Debugger | PyPI | VS Code | Blog | Colab Demo

Signals

GitHub stars
10
Forks
2
Last commit
Aug 2026
Advanced
Delivery
lu-mcp-server MCP server → your ahel gateway (mcp.ahel.ai) → every connected AI client.
Catalog kind
mcp-server
Gateway key
io-github-rafapra3008-lu-mcp-server
Source
github.com/rafapra3008/cervellaswarm