MCP: an assistant can author models with no docs pasted in

[sajonaro]

Implements the feature request in mcp_advanced.md (R1–R8). An LLM client with no Writ knowledge can now learn the language from the server, send models inline, fix errors from the error alone, and be told when a model is too big.

What changes

• Inline sources (R1). Every path argument has a *_source twin, at most 256 KB. Inline text is served as inline:NAME.writ, a name no (load …) can reach, so an inline model can never stand in for a library that pinned claims load. claims_source is refused under --claims-dir. model_name keeps revision history per name for as long as the server runs. Inline writ_compare and writ_query must be given claims, since an inline model has no sibling .claims file.
• writ_guide (R2). Topics index, syntax.model, syntax.claims, syntax.rules, semantics (it answers the request's 11 questions), idioms, and five worked examples: mutex, webhooks, consumer, commit, handoff. Each example shows the failing check, the fix and the compare. There is also one topic per error code. The topics are markdown in tooling/mcp/guide/, compiled into the server. The largest is about 2k tokens.
• Instructions, inline example, resources, prompt (R3, R4, R8).
• writ_validate (R5). Parses and type-checks without building the space, then summarises types, arrows, laws, moves, properties and relations, plus the situation bound. It warns when the bound is over budget. A misspelt name in claims, which writ_check would answer n/a, is an error here.
• Coded errors (R6). Each error carries a code, its source, line and column, found and expected names, a hint, a corrected fix line for a misspelt name, and a pointer to its guide topic. Codes are assigned in one table (diagnose.ml), and a test proves each code's wrong example still raises it. One error per file: the front ends stop at the first.
• Limits (R7). max_situations (default 200000, at most 2000000) and timeout_ms (default 60000). A search that is cut off returns E_STATE_LIMIT with how far it got, the bound, every property marked undecided, and the cells that grew most.
• writ_compare now ends with the properties still failing in both models, so a fix that fixed nothing doesn't look clean.
• Matches 0.4.0. The MCP check counts n/a as a finding, as writ check now does.

Breaking

A transition clause other than when or do is now an error. A bare (set …) outside (do …) used to be dropped silently, leaving a move that changed nothing. None of the 70 models across writ, writ-problems, writ-arch and writ-scheduling-verification has one.

Also

docs/interrogator.md §2's can-reach base case lacked (situation S); holds does not bind its situation, so the rule was rejected.

Also: report readability and certification

• A failing inevitable shows how a run avoids its goal. It prints avoids: the run stops at #N when the run stops, or loop: the shortest cycle back to the stuck situation. Under (fair …) it prints loops among: the situations a fair run circles in.
• Long dead-end lists are shortened in the text report. A route of more than 24 moves keeps its first and last 10 and gives the count of the rest; after 20 dead ends the report gives the count of the remainder. --json still lists every dead end.
• certified no longer suggests n/a claims were checked. When every property is n/a and no query was asked, the line reads certified: the situation count only — every property is n/a, so no claim was checked. This applies to both writ check and writ_check.
• None of these change --json or the certificate format, so writ-cert needs no change.
• The plugin's SKILL.md mentions writ_guide and writ_validate for servers that list them. It still reads correctly against the pinned 0.4.0 image.

Testing

• make build, make lint and make test pass. test_mcp_authoring has 231 checks: it re-runs every guide example against its printed output, and every error code's wrong and right example. test_report_json covers the n/a certified line.
• A fresh agent was given only the tools, with no server instructions. It passed the six acceptance scenarios: cold authoring, error recovery, property kinds, regression catch, witness inspection, and too-large. Its findings and a separate code review are fixed in this PR.
• make downstream: all six suites pass (problems, crosscheck, arch, scheduling, mgtt2writ, vscode) with PROBLEMS_REF=queens-count-from-json. Merge queens: count complete boards from --json writ-problems#15 first. Its queens check counted the complete boards in the text dead-end list, which this PR now cuts off at 20.

🤖 Generated with Claude Code