검증된 AI 에이전트 프로토콜을 위한 언어.
브라우저에서 체험하기 -- 설치가 필요 없습니다. AI 에이전트 실시간 보기 -- 검증된 프로토콜에서 3개의 에이전트가 작동합니다.
AI 에이전트들은 서로 대화하지만, 그들이 규칙을 따르는지 보장할 방법이 없습니다. 잘못된 발신자, 잘못된 메시지 순서, 누락된 단계 등은 운영 환경에서야 발견됩니다.
Lingua Universale(LU)은 AI 에이전트 대화를 위한 타입 체커입니다. 프로토콜을 정의하면 LU가 그 정확성을 증명하고, 런타임이 이를 강제합니다.
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프로토콜에 따르면 검토자가 다음 차례여야 합니다. 런타임은 이를 차단합니다. 코드를 신뢰해서가 아니라, 세션 타입이 이를 불가능하게 만들기 때문입니다.
Related MCP server: edict-lang
pip install cervellaswarm-lingua-universale또는 먼저 체험해 보세요: 플레이그라운드 (Pyodide를 통해 브라우저에서 실행).
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그런 다음 검증하세요:
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.수학적 증명입니다. 오늘 통과하고 내일 실패하는 테스트가 아닙니다.
기능 | 설명 |
전체 컴파일러 | 토크나이저, 파서(64개 규칙), AST, 계약 체커, Python 코드 생성 |
9가지 검증 속성 |
|
20개 표준 라이브러리 프로토콜 | AI/ML, 비즈니스, 통신, 데이터, 보안 등 즉시 사용 가능 |
린터 + 포맷터 |
|
LSP 서버 | 진단, 호버, 자동 완성, 정의로 이동, 포맷팅 |
VS Code 확장 프로그램 | |
대화형 채팅 |
|
브라우저 플레이그라운드 | 지금 체험하기 -- 확인, 린트, 실행, 채팅 |
Lean 4 브리지 | 수학적 증명 생성 및 검증 |
REPL | 대화형 탐색을 위한 |
프로젝트 스캐폴딩 | 20개의 검증된 템플릿에서 |
37개 모듈. 3979개 테스트. 외부 의존성 제로. 순수 Python 표준 라이브러리.
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 serverGitHub Actions 워크플로우에 프로토콜 검증을 추가하세요:
# .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/위반 시 종료 코드가 0이 아니므로 모든 CI 시스템과 호환됩니다.
LU는 다자간 세션 타입(Honda, Yoshida, Carbone -- POPL 2008)을 기반으로 합니다. 세션 타입은 통신 프로토콜을 타입으로 설명합니다. 두 프로세스가 동일한 세션 타입을 따르면 데드락이 발생하지 않고, 메시지가 잘못된 순서로 도착하지 않으며, 대화가 항상 종료됩니다.
파이프라인:
.lu source → Tokenizer → Parser → AST → Spec Checker → Lean 4 Proofs → Python Codegen
↓
PROVED or VIOLATEDLU는 기존 AI 에이전트 프레임워크를 대체하지 않습니다. 더 안전하게 만들어 줄 뿐입니다. JavaScript를 위한 TypeScript처럼, 기존 도구는 유지하면서 보증을 추가하는 것입니다.
LU 디버거 -- 실시간 웹 앱: 3개의 AI 에이전트(고객, 창고, 결제)가 검증된 OrderProcessing 프로토콜로 통신합니다. "Break"를 클릭하여 실시간으로 차단되는 프로토콜 위반을 확인하세요. 소스 코드.
examples/ 디렉토리를 확인하세요:
에이전트 오케스트레이션 -- 중첩된 선택이 있는 3개의 AI 에이전트, 8/8 속성 증명 완료
라이브 러너 -- 검증된 프로토콜상의 실제 Claude API 에이전트
표준 라이브러리 -- 5개 카테고리에 걸친 20개의 검증된 프로토콜
또는 대화형 Colab 노트북을 시도해 보세요 -- 2분 소요, 설정 불필요.
Lingua Universale은 CervellaSwarm의 핵심 프로젝트입니다. 또한 다음 Python 패키지들을 게시하고 있습니다:
패키지 | 기능 |
AST 기반 코드 이해 (tree-sitter, PageRank) | |
Claude Code 에이전트를 위한 라이프사이클 훅 | |
에이전트 정의 템플릿 및 팀 구성 | |
결정론적 작업 라우팅 및 검증 | |
다중 에이전트 프로세스 관리 | |
대화 간 지속적인 세션 컨텍스트 | |
불변 이벤트 로깅 및 감사 추적 | |
자동화된 품질 검사 및 점수 산정 |
모두 Apache 2.0 라이선스, Python 3.10+ 지원, 테스트 완료 및 문서화되어 있습니다.
기여를 환영합니다! 가이드라인은 CONTRIBUTING.md를 참조하세요.
버그 리포트: GitHub Issues
보안: 책임 있는 공개에 대해서는 SECURITY.md를 참조하세요
Apache License 2.0 -- LICENSE를 참조하세요.
Copyright 2025-2026 CervellaSwarm Contributors.
Lingua Universale -- AI 에이전트를 위한 검증된 프로토콜.
Verify the formal safety properties declared in a .lu protocol.
Runs the static property checker (Layer 1) on all protocols found in
the source. Optionally, if Lean 4 is installed, also runs formal
verification (Layer 2).
Args:
protocol_text: Full .lu protocol definition text including a
"properties:" block, e.g.:
" properties:\n"
" always terminates\n"
" no deadlock\n"
" all roles participate\n"
Returns:
JSON string with:
ok (bool), protocols (list of protocol results), summary (dict).
Each protocol result has: protocol_name, all_passed, results (list).
Each result has: kind, verdict, evidence, params.
| Name | Required | Description | Default |
|---|---|---|---|
| protocol_text | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden. It discloses running the static checker on all protocols and the optional Lean verification, including the prerequisite of Lean installation. No contradictions or missing critical behavioral details.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with an intro, argument explanation, and return value specification. It is relatively concise and front-loaded, though slightly lengthy. Every sentence adds value.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's simplicity (one parameter, output schema exists), the description is complete. It explains the input format, optional behavior, and return structure in sufficient detail. No gaps.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0%, so the description compensates by explaining the 'protocol_text' parameter in detail, including example format and requirement for a 'properties' block. This adds significant meaning beyond the schema which only defines it as a string.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: verifying formal safety properties in .lu protocols. It specifies static checking and optional Lean verification, distinguishing it from sibling tools like lu_list_templates, lu_load_protocol, and lu_verify_message.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explains when to use the tool (to verify properties) and mentions optional Lean verification if installed. It does not explicitly exclude scenarios, but the context is sufficiently clear.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
List available Lingua Universale standard library protocol templates.
The standard library contains 20 verified protocols across 5 categories:
communication, data, business, ai_ml, security.
Args:
category: Optional filter. One of: communication, data, business,
ai_ml, security. Leave empty to list all templates.
Returns:
JSON string with:
ok (bool), templates (list), category_filter (str), total (int).
Each template has: name, category, description.
| Name | Required | Description | Default |
|---|---|---|---|
| category | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden. It describes the return structure (JSON with ok, templates, category_filter, total) and the number of templates and categories. It does not cover error handling or edge cases, but for a read-only list tool this is sufficient.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with Args and Returns sections, each sentence adds value. It is concise yet complete, with no redundant information.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's simplicity (list with optional filter), the description covers all necessary context: purpose, parameter usage, and return format. No additional information is needed for correct invocation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0%, but the description fully compensates by specifying the allowed values for the category parameter and explaining the default behavior (empty lists all). This adds essential meaning beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool lists available Lingua Universale standard library protocol templates, specifying the resource and action. It distinguishes from sibling tools (check, load, verify) by focusing on listing.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It provides clear guidance on using the optional category filter, including the list of allowed categories and that leaving it empty lists all. However, it does not explicitly state when not to use this tool versus alternatives, though the context of siblings makes it clear.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Parse a Lingua Universale (.lu) protocol definition.
Accepts the full text of a .lu file and returns the parsed protocol
structure: name, roles, steps, choices, and declared properties.
Args:
protocol_text: Content of a .lu file, e.g.:
"protocol RequestResponse:\n"
" roles: client, server\n"
" client asks server to process request\n"
" server returns response to client\n"
" properties:\n"
" always terminates\n"
" no deadlock\n"
Returns:
JSON string with keys:
ok (bool), protocol_name (str), roles (list[str]),
steps (list), properties (list), error (str on failure).
| Name | Required | Description | Default |
|---|---|---|---|
| protocol_text | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
The description discloses the operation is a parsing action with no side effects, includes error handling, and fully covers behavior since no annotations are present.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is well-structured with Args and Returns sections, including a helpful example, though slightly lengthy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description is complete for a simple tool with one parameter and no output schema, covering input format and output keys.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Despite 0% schema description coverage, the description provides a clear example and explains the input format (full text of .lu file), adding significant meaning beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description states it parses a .lu protocol definition and returns the parsed structure, clearly differentiating from sibling tools like lu_check_properties and lu_list_templates.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage for loading a protocol from text but lacks explicit guidance on when to use alternatives or when not to use.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Verify whether a message is valid in the context of an ongoing session.
Replays the existing message history against the protocol, then checks
whether next_message is the expected next step.
Args:
protocol_text: Full .lu protocol definition text.
messages: List of already-sent messages, each a dict with keys:
sender (str), receiver (str), action (str).
Actions are LU action names: "asks", "returns", "sends",
"proposes", "tells". These match the verbs in .lu source files.
next_message: The message to validate, same format as above.
Returns:
JSON string:
On success: {"valid": true, "step": N, "next_expected": "..."}
On violation: {"valid": false, "violation": "...", "expected": "...", "got": "..."}
On error: {"valid": false, "error": "..."}
Example:
protocol_text = "protocol Ping:\n roles: a, b\n a asks b to ping\n b returns pong to a\n properties:\n always terminates\n"
messages = [{"sender": "a", "receiver": "b", "action": "asks"}]
next_message = {"sender": "b", "receiver": "a", "action": "returns"}
# Returns: {"valid": true, ...}
| Name | Required | Description | Default |
|---|---|---|---|
| protocol_text | Yes | ||
| messages | Yes | ||
| next_message | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided, so description carries full burden. It details the replay-and-check algorithm, parameter semantics, and full return format. It does not mention side effects, but as a verification tool, none are expected.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Description is well-structured: purpose sentence, then detailed argument descriptions, return format, and example. Slightly lengthy due to example but front-loaded and each section earns its place.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given 3 required nested parameters with 0% schema coverage and an output schema described in text, the description provides complete information: argument formats, valid actions, return types, and a concrete example. An agent can invoke correctly.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema has 0% description coverage, but the description fully compensates by explaining each parameter: protocol_text is .lu protocol text, messages list with required keys, next_message same format, with example action values. Adds significant meaning beyond schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool verifies if a message is valid given a protocol and message history, using verbs like 'verify' and 'replays'. It is distinct from siblings that check properties, list templates, or load protocols.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explains the context ('in the context of an ongoing session') and the process (replaying history, checking next step). It does not explicitly state when not to use or alternatives, but siblings are sufficiently different, making intended use clear.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v1.0.0lu_check_propertieslu_list_templateslu_load_protocollu_verify_messageScored across 4 tools
Each tool has a distinct purpose: parsing, message verification, property checking, and template listing. No overlap in functionality; agents can easily select the right tool for their task.
Names follow a consistent 'lu_' prefix and verb_noun pattern (load_protocol, verify_message, check_properties, list_templates). Minor deviation: 'load_protocol' could be 'parse_protocol' but still clear and consistent.
With only 4 tools, the server is slightly under the typical 3-15 range, but this is appropriate for a niche protocol validation domain. The tools cover the core needs without bloat.
The server covers parsing, verification, property checking, and template listing, but misses a 'simulate' or 'validate full session' tool. Gaps exist for agents needing end-to-end protocol simulation or editing, but core workflows are supported.
Tamper-evident proof creation and verification for AI agents via MCP, A2A, and REST.
The team layer for AI coding agents: shared contracts, collision alerts, E2EE sessions.
Pre-execution governance for AI agents. Deterministic PASS/FAIL/REVIEW verdicts, replayable proof.
Zero-trust gateway for AI agents: score tool calls, verify agent cards, enforce policy, audit.
