← 返回 Skills 市场
rafapra3008

Lingua Universale Protocol Verification

作者 rafapra3008 · GitHub ↗ · v0.1.0 · MIT-0
cross-platform ✓ 安全检测通过
211
总下载
0
收藏
0
当前安装
1
版本数
在 OpenClaw 中安装
/install lingua-universale
功能描述
Verify agent-to-agent communication against session type protocols. Mathematical proofs, not trust.
使用说明 (SKILL.md)

Lingua Universale - Protocol Verification Skill

What it does

Verifies that agent-to-agent messages follow a formally defined protocol using session types -- the same mathematical framework used in distributed systems research (Honda/Yoshida POPL 2008, Scribble, MPST).

No API keys required. No external services. Runs entirely locally.

When to use

  • Before sending a message to another agent: confirm the message is expected
  • After a conversation: validate the full transcript against the protocol
  • During design: check safety properties (no deadlock, always terminates)
  • When choosing a protocol pattern: browse 20 standard library templates

Tools provided

lu_load_protocol

Parse a .lu protocol definition and extract its structure.

Input: protocol_text (string) -- full content of a .lu file Output: JSON with protocol name, roles, steps, choices, and declared properties

lu_verify_message

Check if a message is valid in the context of an ongoing session.

Input:

  • protocol_text (string) -- the protocol definition
  • messages (list) -- already-sent messages: [{"sender": "a", "receiver": "b", "action": "ask"}]
  • next_message (dict) -- message to validate: {"sender": "b", "receiver": "a", "action": "return"}

Output: {"valid": true, "next_expected": "..."} or {"valid": false, "violation": "...", "expected": "...", "got": "..."}

lu_check_properties

Verify the formal safety properties declared in a protocol.

Input: protocol_text (string) Output: JSON with per-property verdicts (PROVED / SATISFIED / VIOLATED / SKIPPED) and evidence

Supported properties:

  • always terminates -- no infinite loops
  • no deadlock -- no role waits forever
  • no deletion -- no destructive operations
  • X before Y -- message ordering constraint
  • role cannot send message -- exclusion
  • role exclusive message -- only this role may send this message
  • confidence >= level -- minimum confidence threshold
  • trust >= tier -- minimum trust tier
  • all roles participate -- every role sends at least one message

lu_list_templates

Browse the 20 protocols in the Lingua Universale standard library.

Input: category (optional string) -- filter by: communication, data, business, ai_ml, security Output: JSON with template names, categories, property highlights, and usage instructions

Example workflow

# 1. Choose a protocol template
lu_list_templates(category="ai_ml")
# -> rag_pipeline, agent_delegation, tool_calling, human_in_loop, consensus

# 2. Load and inspect the protocol
lu_load_protocol("""
    protocol AgentDelegation:
        roles: supervisor, worker, validator
        supervisor asks worker to execute task
        worker returns result to supervisor
        supervisor asks validator to audit result
        validator returns verdict to supervisor
        properties:
            always terminates
            no deadlock
            all roles participate
            trust >= standard
""")

# 3. Verify messages as they flow
lu_verify_message(
    protocol_text=\x3Cabove>,
    messages=[
        {"sender": "supervisor", "receiver": "worker", "action": "ask"}
    ],
    next_message={"sender": "worker", "receiver": "supervisor", "action": "return"}
)
# -> {"valid": true, "next_expected": "supervisor -> validator : audit_request"}

# 4. Check formal properties
lu_check_properties(\x3Cprotocol_text>)
# -> all_passed: true, PROVED: always terminates, no deadlock, all roles participate

Protocol syntax (.lu)

protocol Name:
    roles: role1, role2, role3

    role1 asks role2 to do something
    role2 returns result to role1

    when role1 decides:
        approve:
            role1 tells role3 about decision
        reject:
            role1 sends error to role3

    properties:
        always terminates
        no deadlock
        all roles participate

Valid actions: asks, returns, sends, proposes, tells

Installation

# As a Claude Code MCP server
uvx openclaw-skill-lingua-universale

# Or install directly
pip install openclaw-skill-lingua-universale
lu-mcp  # starts stdio MCP server

Academic references

  • Honda, Yoshida, Carbone - "Multiparty Asynchronous Session Types" (POPL 2008)
  • Scribble Project - session type toolchain (Imperial College London)
  • Dezani-Ciancaglini et al. - "Session Types for Access and Information Flow Control" (2021)
安全使用建议
The skill appears coherent for verifying agent protocols locally, but take these precautions before installing/running: (1) inspect the upstream package cervellaswarm-lingua-universale (source on the referenced GitHub) — the skill imports that package and its behavior determines what actually runs; (2) prefer installing and running the MCP server in a sandbox/container or an isolated environment to limit potential supply-chain risks; (3) confirm the uvx MCP server is not exposed to untrusted network endpoints (run it on localhost only) and that you trust the package author/repository; (4) avoid pip installing packages from unknown sources into sensitive environments — if you need high assurance, review the cervellaswarm-lingua-universale source code or vendor it from a vetted source. My confidence is medium because the provided lu_mcp_server.py was truncated in the report and the skill relies on a third-party package that will be pulled at install time; reviewing the full included code and the external package would raise confidence.
功能分析
Type: OpenClaw Skill Name: lingua-universale Version: 0.1.0 The lingua-universale skill bundle provides a formal verification framework for agent-to-agent communication based on session types. The implementation in lu_mcp_server.py acts as a wrapper for the cervellaswarm-lingua-universale library, exposing tools for parsing protocols, verifying message sequences, and checking safety properties (e.g., deadlock freedom). The code and SKILL.md instructions are well-documented, align with the stated purpose of mathematical protocol verification, and show no signs of data exfiltration, malicious execution, or harmful prompt injection.
能力评估
Purpose & Capability
Name, description, tools (lu_load_protocol, lu_verify_message, lu_check_properties, lu_list_templates), and required binary (uvx) align: uvx is used to run the MCP server and the package depends on cervellaswarm-lingua-universale for the verification logic. No unrelated credentials, binaries, or config paths are requested.
Instruction Scope
SKILL.md provides narrowly-scoped instructions for parsing .lu files, replaying message histories, and checking properties. It does not instruct the agent to read unrelated files, environment variables, or to send data to external endpoints. The install/run guidance (uvx openclaw-skill-lingua-universale or pip install + lu-mcp) is explicit and limited to running the MCP server locally.
Install Mechanism
The registry entry has no automated install spec, but SKILL.md and pyproject recommend pip installing openclaw-skill-lingua-universale and the package depends on cervellaswarm-lingua-universale>=0.3.3. Installing via pip will pull a third-party package from PyPI (supply-chain risk) — there is no download-from-arbitrary-URL behavior in the skill files themselves.
Credentials
The skill declares no required environment variables, no credentials, and no config paths. The code shown does not access secrets or unrelated env vars. This is proportionate to a local verification tool.
Persistence & Privilege
always is false; the skill does not request permanent/global presence or to modify other skills' configurations. It runs as an MCP server (local process) which is the expected runtime model; autonomous invocation is allowed (normal) but not elevated.
如何使用
  1. 确保已安装 OpenClaw(本地或 Docker 部署)
  2. 在对话框中输入安装命令:/install lingua-universale
  3. 安装完成后,直接呼叫该 Skill 的名称或使用 /lingua-universale 触发
  4. 根据 Skill 的参数说明提供必要输入,即可获得结构化输出
版本历史
v0.1.0
4 MCP tools: formal protocol verification for AI agent communication. Session types + Lean 4 proofs.
元数据
Slug lingua-universale
版本 0.1.0
许可证 MIT-0
累计安装 0
当前安装数 0
历史版本数 1
常见问题

Lingua Universale Protocol Verification 是什么?

Verify agent-to-agent communication against session type protocols. Mathematical proofs, not trust. 它是一个面向 Claude Code / OpenClaw 的 AI Agent Skill 插件,目前累计下载 211 次。

如何安装 Lingua Universale Protocol Verification?

在 OpenClaw 或 Claude Code 对话框中运行命令「/install lingua-universale」即可一键安装,无需额外配置。

Lingua Universale Protocol Verification 是免费的吗?

是的,Lingua Universale Protocol Verification 完全免费,采用 MIT-0 许可证,可自由下载、安装和使用。

Lingua Universale Protocol Verification 支持哪些平台?

Lingua Universale Protocol Verification 跨平台运行,可在任意部署了 OpenClaw / Claude Code 的环境中使用(cross-platform)。

谁开发了 Lingua Universale Protocol Verification?

由 rafapra3008(@rafapra3008)开发并维护,当前版本 v0.1.0。

💬 留言讨论