Model the agent loop as the architecture describes it

A Quint model of the design in docs/Architecture.md (PR #90): intake,
restatements and go-aheads, park-and-switch, blocked dependencies,
harness-owned milestones, waiting for merges, review follow-ups, record
issues, crashes and build VM wipes. It found five gaps; the model carries
the proposed fixes, and loop_scenarios.qnt keeps each counterexample.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

specs/README.md

@@ -36,3 +36,35 @@ Exhaustive bounded checking (`quint verify`) uses Apalache and needs Java 17.
 left, change the matching function here in the same PR. When a
 counterexample's fix lands, flip its scenario's `expect` to the property
 holding, and drop the `xfail` from its Python reproduction.
+
+## `loop.qnt`: the agent loop, as the architecture describes it
+
+Models the design in `docs/Architecture.md` rather than code, since the new
+loop doesn't exist yet:
+- work items from assigned issues and conversations;
+- restatements and revision-bound go-aheads;
+- park-and-switch, with branches pushed on parking;
+- blocked dependencies;
+- harness-owned milestones and waiting for merges;
+- review follow-ups;
+- record issues;
+- crashes and build VM wipes at any point.
+
+A counterexample here is a gap in the architecture, so it is fixed there,
+and the model carries the fix (marked `FIX n`). `loop_scenarios.qnt` keeps each
+counterexample as a trace of the fixed behaviour. Each trace fails if its fix
+is reverted, and each property that never failed was checked against a
+deliberately broken model.
+
+```sh
+quint run specs/loop.qnt --invariant=all_properties --max-steps=80 --max-samples=200000
+quint test specs/loop_scenarios.qnt
+```
+
+Traces need about 80 steps to reach second milestones. The `w_*` values at the
+end are reachability witnesses: each should be *violated*, which shows the
+state it names is reachable.
+
+**Keeping it true.** When the architecture changes a rule this models, change
+the model in the same PR. When the new loop is built (Development Plan Phase 2),
+each property gets a test against the real code, as `orchestrator.qnt`'s did.