dongarandClaude Opus 5.5
6ae2375194
nisse-dev now runs only the conversational loop. The gated state machine it was built alongside is gone: - Removed control.py, planner.py, executor.py, approvals.py, gates.py (command_form moves to loop/reader.py), publish.py and poller.py, the old assembly in agent.py (its shared helpers move to loop/build.py), the store's state-machine view (get_state, transition), their tests, the old end-to-end and live planning/milestone/gate tests, and specs/orchestrator.qnt with its scenarios. - Roles are driver, helper, expert and classifier; driver is required. loop:, roles.planner, roles.executor and tuning.executor are refused with what to use instead; tuning.driver takes the turn cap and failure limit. - The benchmark and the capability matrix measure the driver: the loop's own system prompt and tools, the task's plan as the agreed restatement. Task plans end with finish_milestone, so earlier runs show as (old); stored runs' executor tuning reads as the driver's. - A delegation on the loop records what its helper's alias resolved to (L9), as the old path's did. - The dump shows a work item's revision and what it waits for. - Behaviour the old tests covered and the loop shares stays covered: driver runs that fail on a model call, stop mid-turn, reset the failure count; go-aheads ignoring case and punctuation; a request too big to fit is never sent; the assembly tests, now on build_loop_agent. 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.
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.