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).

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, ...}

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.

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.