cervellaswarm-lingua-universale 0.2.0

The first programming language designed for AI — session types, compiler, REPL, and formal verification

CervellaSwarm Lingua Universale

The first programming language designed for AI. By AI.

A complete language — grammar, compiler, REPL, LSP server, and formal verification — built entirely on the Python standard library. Zero external dependencies.

pip install cervellaswarm-lingua-universale

---

What Is Lingua Universale?

Lingua Universale (LU) is a programming language where the question and the answer live in the same language. It models AI agent communication with precision: who sends what to whom, under what contracts, with what confidence.

It started as a session types library. It is now a full language:

• Grammatica: 62 production rules, formal EBNF, Lark + GBNF export
• Compilatore: tokenizer -> AST -> contract checker -> Python codegen
• REPL: interactive session with history and error recovery
• LSP: Language Server Protocol server for editor support
• Verifica formale: Lean 4 theorem generation and auto-verification
• Errori umani: 74 error codes in 3 languages (en/it/pt)

---

Quick Start

Python API

from cervellaswarm_lingua_universale import (
    SessionChecker, DelegateTask, TaskRequest, TaskResult, TaskStatus,
)

# Define a typed message
request = TaskRequest(
    task_id="T001",
    description="Fix the login bug",
    target_files=("src/auth.py",),
)

# Start a protocol-checked session
checker = SessionChecker(DelegateTask)
checker.send("regina", "worker", request)  # OK: protocol expects TaskRequest here

# Worker responds with the correct type
result = TaskResult(task_id="T001", status=TaskStatus.OK, summary="Fixed null check")
checker.send("worker", "regina", result)   # OK: protocol expects TaskResult here

# Wrong message? Caught immediately.
checker.send("worker", "regina", request)
# raises ProtocolViolation: expected sender=regina, got sender=worker

.lu Files

Write protocols in the LU language and run them directly:

# hello.lu
agent Regina role=coordinator
agent Worker role=executor

protocol Greet {
    roles Regina, Worker;
    Regina -> Worker : TaskRequest;
    Worker -> Regina : TaskResult;
}

lu check hello.lu     # parse and compile, no execution
lu run   hello.lu     # parse, compile, and execute
lu repl               # interactive REPL

---

CLI Reference

The lu command ships with 7 subcommands:

Command	Description
lu run <file.lu>	Parse, compile, and execute a .lu file
lu check <file.lu>	Parse and compile without executing (fast lint)
lu verify <file.lu>	Parse, compile, and formally verify with Lean 4
lu compile <file.lu>	Show (or save with -o) the generated Python source
lu repl	Start the interactive REPL with history
lu lsp	Start the LSP server over STDIO (requires pygls)
lu version	Show version and build information

# Check a file and see what was declared
lu check hello.lu
# OK hello.lu
#   2 agent(s), 1 protocol(s)

# Compile to Python and save
lu compile hello.lu -o hello.py

# LSP (install optional dep first)
pip install "cervellaswarm-lingua-universale[lsp]"
lu lsp

---

Features

• 25 modules, 131 public API symbols
• 2828 tests, 98% coverage, runs in under 1 second
• Zero dependencies -- pure Python standard library
• Python 3.10+ including 3.13 free-threaded (thread-safe internals)
• Grammar: 62 production rules, GBNF + Lark export for constrained decoding
• Errors: 74 error codes in 3 languages (English, Italian, Portuguese)

---

Architecture

Lingua Universale v0.2.0 -- 25 modules, zero dependencies

FASE A: Session Types
  types.py           14 MessageKind, 14 message dataclasses, 17 AgentRole
  protocols.py       Protocol, ProtocolStep, ProtocolChoice, 4 standard protocols
  checker.py         SessionChecker: runtime protocol enforcement
  dsl.py             Parse/render Scribble-inspired notation
  monitor.py         6 event types, ProtocolMonitor, MetricsCollector
  lean4_bridge.py    Generate + verify Lean 4 proofs (7 properties)
  integration.py     AgentInfo catalog, create_session, validate_swarm

FASE B: Advanced Types
  confidence.py      ConfidenceScore, Confident[T], 3 composition strategies
  trust.py           TrustScore, TrustTier, transitive compose, attenuation
  codegen.py         Python source generation from protocol AST
  intent.py          Natural language -> protocol intent parser
  spec.py            Property specs, formal checker, session verifier

FASE C: Il Linguaggio (compiler pipeline)
  _tokenizer.py      Lexer: 30+ token types, position tracking
  _ast.py            AST node hierarchy (agents, protocols, types, imports)
  _parser.py         Recursive descent parser, 62 production rules
  _contracts.py      Contract checker: scope, type, arity validation
  _compiler.py       ASTCompiler -> CompiledModule (Python AST)
  _interop.py        compile_file / load_file public API
  _grammar_export.py GBNF + Lark grammar export (constrained decoding)
  _eval.py           check_source / run_source / verify_source
  _repl.py           Interactive REPL with history and error recovery
  _cli.py            lu command: 7 subcommands
  errors.py          74 error codes, 3 locales (en/it/pt), rich snippets
  _colors.py         ANSI colors respecting NO_COLOR / FORCE_COLOR

FASE D: Ecosistema
  _lsp.py            Language Server Protocol (STDIO, requires pygls)

---

Session Types and Protocols

Define who can send what to whom, and in what order:

from cervellaswarm_lingua_universale import Protocol, ProtocolStep, ProtocolChoice, MessageKind

review_protocol = Protocol(
    name="CodeReview",
    roles=("developer", "reviewer", "approver"),
    elements=(
        ProtocolStep("developer", "reviewer", MessageKind.TASK_REQUEST),
        ProtocolChoice(
            decider="reviewer",
            branches={
                "approve": (
                    ProtocolStep("reviewer", "approver", MessageKind.AUDIT_REQUEST),
                    ProtocolStep("approver", "developer", MessageKind.AUDIT_VERDICT),
                ),
                "reject": (
                    ProtocolStep("reviewer", "developer", MessageKind.TASK_RESULT),
                ),
            },
        ),
    ),
)

DSL Notation

Write protocols in human-readable syntax inspired by Scribble (Honda, Yoshida, Carbone, POPL 2008):

from cervellaswarm_lingua_universale import parse_protocol, render_protocol

protocol = parse_protocol("""
protocol CodeReview {
    roles developer, reviewer;

    developer -> reviewer : TaskRequest;

    choice at reviewer {
        approve: {
            reviewer -> developer : AuditVerdict;
        }
        reject: {
            reviewer -> developer : TaskResult;
        }
    }
}
""")

# Round-trip fidelity: parse(render(P)) preserves structure
print(render_protocol(protocol))

---

Confidence Types

Uncertainty as a first-class type -- not a string, not a comment:

from cervellaswarm_lingua_universale import Confident, ConfidenceScore

# Wrap any value with its confidence
result = Confident(
    value="Authentication bug is in line 42",
    confidence=ConfidenceScore(0.85, evidence=("stack_trace", "test_failure")),
)

# Compose confidence through a pipeline
reviewed = result.and_then(lambda finding: Confident(
    value=f"Confirmed: {finding}",
    confidence=ConfidenceScore(0.95),
))

print(reviewed.confidence.value)  # 0.8075 (0.85 * 0.95 -- multiplicative)
print(reviewed.is_high)           # True (>= 0.8)

---

Trust Composition

Model how trust propagates through delegation chains:

from cervellaswarm_lingua_universale import TrustScore, TrustTier, compose_chain

coordinator = TrustScore(value=1.0, tier=TrustTier.VERIFIED)
worker = TrustScore(value=0.75, tier=TrustTier.STANDARD)

# A -> B -> C: trust composes multiplicatively
chain_trust = compose_chain((coordinator, worker))
print(chain_trust.value)  # 0.75
print(chain_trust.tier)   # TrustTier.STANDARD (lower of the two)

# Privilege attenuation: B cannot give C more authority than A gave B
attenuated = worker.attenuate(0.5)
print(attenuated.value)   # 0.375

---

Protocol Monitor

Observe protocol execution with zero overhead when disabled:

from cervellaswarm_lingua_universale import (
    SessionChecker, DelegateTask, ProtocolMonitor, EventCollector,
)

monitor = ProtocolMonitor()
collector = EventCollector()
monitor.add_listener(collector)

checker = SessionChecker(DelegateTask, monitor=monitor)
# ... send messages ...

for event in collector.events:
    print(f"{event.event_type}: {event.timestamp}")

---

Lean 4 Verification

Generate formal proofs that your protocols are correct:

from cervellaswarm_lingua_universale import Lean4Generator, DelegateTask

generator = Lean4Generator()
lean_code = generator.generate(DelegateTask)
print(lean_code)
# Outputs Lean 4 code with theorems:
#   theorem DelegateTask_senders_valid : ...  := by decide
#   theorem DelegateTask_no_self_loop : ...   := by decide
#   theorem DelegateTask_non_empty : ...      := by decide
#   ... (7 properties total)

If Lean 4 is installed, verify automatically:

from cervellaswarm_lingua_universale import Lean4Verifier

verifier = Lean4Verifier()
report = verifier.verify_protocol(DelegateTask)
print(report.all_proved)  # True -- mathematically proven

---

How It Compares

Feature	AutoGen	CrewAI	LangGraph	Lingua Universale
Typed messages	No	No	No	Yes (14 message types)
Protocol enforcement	No	No	No	Yes (runtime checker)
Formal DSL + compiler	No	No	No	Yes (62 grammar rules)
Protocol observability	No	No	Partial	Yes (6 event types)
Lean 4 verification	No	No	No	Yes (7 properties)
Confidence types	No	No	No	Yes (Confident[T])
Trust composition	No	No	No	Yes (transitive)
REPL + LSP	No	No	No	Yes
Constrained decoding export	No	No	No	Yes (GBNF + Lark)
External dependencies	Many	Many	Many	Zero

---

FAQ

What is a session type?

A session type describes the sequence of messages two or more parties exchange. Instead of "send whatever, hope the other side understands", a session type says "first A sends X to B, then B sends Y to A." The checker enforces this at runtime, catching violations immediately with a precise error message.

What is a .lu file?

A .lu source file written in the Lingua Universale language. It can declare agents, protocols, types, and imports. The lu CLI compiles it to Python and can run or formally verify it.

Do I need Lean 4 installed?

No. Lean 4 verification is optional. The core library (types, protocols, checker, DSL, compiler, REPL, confidence, trust) works with zero external tools. Install Lean 4 only if you want mathematical proofs of protocol properties.

Do I need pygls for the LSP?

The LSP server (lu lsp) requires pygls. Install it with: pip install "cervellaswarm-lingua-universale[lsp]" Everything else works without it.

Can I define my own message types and protocols?

Yes. The 14 built-in message types and 4 standard protocols cover common multi-agent patterns, but you can create custom protocols with any roles, any message types, and any branching logic -- both in Python and in .lu files.

How does this relate to academic session types?

This library implements multiparty session types (Honda, Yoshida, Carbone 2008) adapted for AI agent systems. The DSL syntax is inspired by Scribble. The key adaptation: our types model AI-specific concerns like confidence, trust, and audit flows that don't exist in traditional distributed systems.

---

Development

git clone https://github.com/rafapra3008/cervellaswarm.git
cd cervellaswarm/packages/lingua-universale
pip install -e ".[dev]"

# Run tests (2828 tests, < 1s)
pytest

# Run with coverage
pytest --cov=cervellaswarm_lingua_universale --cov-report=term-missing

---

Part of CervellaSwarm

This package is the language engine of CervellaSwarm, a multi-agent AI coordination system with 17 specialized agents. It works completely standalone -- no other CervellaSwarm packages required.

---

References

• Honda, Yoshida, Carbone. Multiparty Asynchronous Session Types. POPL 2008.
• Scribble Project. scribble.org. Protocol description language.
• Josang. Subjective Logic. Springer 2016. Trust composition.
• Lean 4. lean-lang.org. Theorem prover.

---

License

Apache-2.0