rafapra3008/cervellaswarm

**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.
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
Then verify it:
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
---
CI Integration
Add protocol verification to your GitHub Actions workflow:
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 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