dongarandClaude Opus 5.5
1ad0b2147d
Development Plan M0.1. Every section reference in code, tests, specs/, the example config, the tuning guide, and the CLAUDE.md and README files now cites docs/Architecture.md (P, L, D, O, X, Q) instead of the old spec's A-H, and docs/Architecture-Build-Spec.md is deleted (git keeps it). The plan's old-to-new table goes with it. Mostly mechanical, with a per-site choice where one old section split: A4 became L2 where it meant stop/abandon/the loop and L3 where it meant approvals; A10 became L6 in the context-budget code and L7 elsewhere; B2 became D4 for outbound Gitea and publishing and D5 for review intake; 'A3 step N' became the matching step of L8's boot sequence. Comments describing behaviour the architecture drops (planning always escalating, thresholds tuned at an old build step) now describe the current code and point at the Development Plan. docs/Architecture.md gains one line the rewrite missed: intake outages delay but never fail work (old B2), now in L5, where the poller and Matrix code cite it. Comments and docs only; no behaviour change. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
Formal models
Quint models of designs where interleavings matter more than any single code path. A model is a hand-written reading of the code: it finds flaws the design and the code share, not places where the code strays from the design. So every counterexample is also reproduced as a failing test against the real code before anything is changed.
orchestrator.qnt: nisse-dev's control loop
Models nisse-dev/src/nisse_dev/control.py: the states, the gate, pending
questions, Gitea comment cursors, publish intents, and the worker queue.
Operator messages, Gitea comments, planner/executor/publisher outcomes
(exceptions included) and a crash at any point all interleave freely.
Each pure function is named after the method it mirrors.
The properties are at the end of the file (all_properties is their
conjunction). Counterexamples are written out as short traces in
orchestrator_scenarios.qnt, and replayed against the real code in
nisse-dev/tests/test_quint_counterexamples.py.
npm install -g @informalsystems/quint # 0.33 or later
# Random simulation, one property at a time:
quint run specs/orchestrator.qnt --invariant=no_stranding \
--max-steps=40 --max-samples=200000
# The counterexample traces (each expects its property to break):
quint test specs/orchestrator_scenarios.qnt
Exhaustive bounded checking (quint verify) uses Apalache and needs Java 17.
Keeping it true. When control.py changes how a state is entered or
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.