dongarandClaude Opus 5.5
a921b73d34
M4.3's block, with new triggers and a way out. A VM out of reach at the check before a run, in a run (which ends there: the driver, a toolchain step and a requested step), or while preparing the workspace blocks every project on it; the item stays ready, waiting on no one. On the intake round it is tried again every tuning.build_vm.retry_s (300), and once it answers it must still answer settle_s (180) later; then the work a lost run left there is parked (pushed), the VM unblocked, and that said once. A changed host key, at the check or on a retry, blocks the VM too, until the operator's `vm ready`, which trusts the new key: `trust new host key` is retired, and the message says it's a key problem that may be an impersonation. Questions are answered while a VM is blocked, without it. Starting the agent with a VM down no longer fails. The walk breaks the VM's SSH, now or partway through a run, and checks that no model works on a VM that is down; loop.qnt models the VM going and coming back (unblocked_only_when_up). Together they found: a lost run's work set aside by the next item there; a question left behind a block; a lost VM swallowed while the toolchain step checked or recorded it; and a remark waiting to be answered that outlived its PR's merge. All fixed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J5Utyfzw7gF7UhjRDEtjTk
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.
npm install -g @informalsystems/quint # 0.33 or later
Exhaustive bounded checking (quint verify) uses Apalache and needs Java 17.
The gated state machine the agent ran before the switch-over (M2.8) had its
own model, orchestrator.qnt; it went with that code, and is in the history.
loop.qnt: the agent loop, as the architecture describes it
Models the design in docs/Architecture.md rather than the code (it was
written before the loop was):
- 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.
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.
Against the real code. nisse-dev/tests/test_loop_properties.py checks
the same properties against the loop itself: a seeded random walk over
what the operator and Gitea can do (go-aheads, answers, comments, merges,
closes, abandon, a crash and restart), checking every property after every
step. It found two bugs the design model couldn't, because they were in the
code: abandon left an open PR, and a review fix after a follow-up PR went to
the merged branch. Each also has its own regression test.
Keeping it true. When the architecture changes a rule this models, change the model and the walk in the same PR.