A model is one page: the kinds of things that exist, the arrows between them, the laws those arrows must obey, and the moves that are allowed. What it means is every situation those rules can produce — that page writ large.

writ builds all of it and answers your questions by exhaustion. So "this can never happen" is a census rather than a search that gave up, and every verdict arrives with a concrete route as evidence.

The river crossing — a farmer, a wolf, a goat, a cabbage, one boat:

$ writ check river.writ --claims river.claims
states: 36   edges: 76
holds  solvable
  witness:  1. cross-goat-LR   2. cross-empty-RL   3. cross-wolf-LR
            4. cross-goat-RL   5. cross-cabbage-LR 6. cross-empty-RL
            7. cross-goat-LR
fails  no-blunders
  stuck at: (farmer.at=right wolf.at=left goat.at=left cabbage.at=left)
  witness:  1. cross-empty-LR

It proves the crossing is possible and prints one — including bringing the goat back on move 4. Then it finds the blunder: one careless first move, after which the crossing can never succeed. Neither answer is a guess, and neither needed a depth bound.

The language is twenty-six words. Everything else — ordering, quantifiers, equality, whole domain vocabularies — is a library built over them. Questions live apart from models, so one question suite can be put to many models, and comparing two versions is a tool operation rather than a reading exercise.

• writ — the language, the engine, the CLI, the LSP and MCP servers, the standard library.
• writ-problems — worked models: puzzles, scheduling, institutional scenarios, and a runner that checks every answer.
• writ-arch — architecture design by exhaustion: a component bank and a brief become every design the constraints permit, with C4 diagrams and decision records that cannot drift.
• writ-scheduling-verification — one tool makes the timetable, another judges it: CP-SAT solves, writ audits, having never seen how the answer was produced.
• writ-vscode — the editor client: diagnostics, outline, hover and completion, served by the engine itself.

opam pin add writ git+https://github.com/writ-lang/writ.git
writ --version

Then the tour — ten runnable steps from a three-line model to the whole language, ending in a one-page cheat sheet.

There are no numbers, no loops and no recursion, and that is the point: it is what makes the negative answer worth having. A domain that cannot be honestly reduced to finitely many named distinctions is one to point a different tool at.