← Back to Skills Marketplace
rafapra3008

Lingua Universale Protocol Verification

by rafapra3008 · GitHub ↗ · v0.1.0 · MIT-0
cross-platform ✓ Security Clean
211
Downloads
0
Stars
0
Active Installs
1
Versions
Install in OpenClaw
/install lingua-universale
Description
Verify agent-to-agent communication against session type protocols. Mathematical proofs, not trust.
README (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)
Usage Guidance
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.
Capability Analysis
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.
Capability Assessment
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.
How to Use
  1. Make sure OpenClaw is installed (local or Docker)
  2. Run the install command in chat: /install lingua-universale
  3. After installation, invoke the skill by name or use /lingua-universale
  4. Provide required inputs per the skill's parameter spec and get structured output
Version History
v0.1.0
4 MCP tools: formal protocol verification for AI agent communication. Session types + Lean 4 proofs.
Metadata
Slug lingua-universale
Version 0.1.0
License MIT-0
All-time Installs 0
Active Installs 0
Total Versions 1
Frequently Asked Questions

What is Lingua Universale Protocol Verification?

Verify agent-to-agent communication against session type protocols. Mathematical proofs, not trust. It is an AI Agent Skill for Claude Code / OpenClaw, with 211 downloads so far.

How do I install Lingua Universale Protocol Verification?

Run "/install lingua-universale" in the OpenClaw or Claude Code chat to install it in one step — no extra setup required.

Is Lingua Universale Protocol Verification free?

Yes, Lingua Universale Protocol Verification is completely free, licensed under MIT-0. You can download, install and use it at no cost.

Which platforms does Lingua Universale Protocol Verification support?

Lingua Universale Protocol Verification is cross-platform and runs anywhere OpenClaw / Claude Code is available (cross-platform).

Who created Lingua Universale Protocol Verification?

It is built and maintained by rafapra3008 (@rafapra3008); the current version is v0.1.0.

💬 Comments