`api_protocol_check`

Exhaustively explore a protocol-case-1.0 finite domain against compiled transaction handlers. Requests carry instance and delivery identities; serializable transactions are atomic; commit-unknown branches into committed and uncommitted durable states; external dispatch and response are separate transitions. Declare IO[Bool] invariants over immutable before/after views, required reachability witnesses, typed named inputs, times, external results, and budgets. Holds means only the complete declared finite domain; violated includes a sourced schedule; exhausted budgets and unsupported semantics are inconclusive. Adapter conformance, authenticated principals and absence of unlisted writers remain explicit assumptions. Use the same case with yichus protocol --case case.json files.bosatsu. Case schema, selector vocabulary and a runnable example: docs/protocol-verification.md (https://github.com/snoble/yichus/blob/main/docs/protocol-verification.md).

Kind: ProtocolCheck. Origin: Yichus/Mcp::catalog.

CLI: yichus protocol — the same finite protocol case and bounded scheduler; the CLI reads the case from --case.

Parameters

sources (required, array) — JSON array of {fileName, source} Bosatsu handlers and declared invariant functions.
case (required, object) — JSON object or encoded JSON string in protocol-case-1.0 format; all domains, assumptions, invariants and bounds are explicit.

Read the result according to this tool’s scope: static checks, bounded execution checks, and descriptive diagrams answer different questions. A successful call is not a general approval of the program. The safety and permissions guide compares the checks and provides editable ownership, guard, and role examples.