lu_check_properties
Verify formal safety properties in .lu protocols by running static property checking and optional formal verification to ensure protocol correctness.
Instructions
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.Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| protocol_text | Yes |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |