Model the orchestrator in Quint, and reproduce its counterexamples #73

2026-09-29T18:52:00Z

dev-agent commented

2026-09-29 18:52:00 +00:00

A Quint model of nisse-dev's control loop, used to search for counterexamples. No behaviour changes: the fixes follow as separate PRs.

The model (specs/orchestrator.qnt, notes in specs/README.md)

Covers control.py's states, the gate, pending questions, Gitea comment cursors, publish intents and the worker queue. Each pure function is named after the method it mirrors.
Interleaves freely: operator messages (every command and free text), comments on the plan issue and the PR, planner/executor/publisher outcomes including exceptions, and a crash at any point. Publishing is split into its four steps so a crash can land between them.
Eight properties. Each message records the plan the operator had seen when sending it, so the model can tell when an approval lands on the wrong plan.

Results: seven counterexamples. Each is written out as a short trace in specs/orchestrator_scenarios.qnt and reproduced against the real code in nisse-dev/tests/test_quint_counterexamples.py, marked xfail(strict=True) until fixed. Each test was checked to fail on its own assertion, not a harness error.

#	Trace	Real behaviour
1	"approve" sent twice, both queued	the second approves the milestone plan, never shown
2	"approve rev-1" meant for the architecture	approves milestone-1 rev-1: tags carry no gate name
3	approve in Matrix and on the Gitea issue	the queued Gitea approval approves the next plan
4	"approve" plus an afterthought	the note rejects the milestone plan, which is re-planned
5	crash after the PR opens, before `PR_OPEN`	restart → `continue` → `start` publishes again; Gitea refuses; no way back to `PR_OPEN`
6	crash while answering a review comment	the comment is never answered, and nobody is told
7	`project complete`	the plan issue is left open (`abandon` closes it)

What held: no_stranding, await_input_has_a_question and execution_needs_approval over 200,000 random traces of up to 40 steps each, and under Apalache's exhaustive check to depth 8. That depth is shallow, but Apalache does find counterexample 1 within it, so the search is exhaustive at that depth.

Limits: the model is hand-written from the code. It finds flaws the design and code share, not places where the code strays from the design; that's why each result is also reproduced against the real code. CI doesn't run Quint: it needs Node for the simulator and Java 21 for Apalache. specs/README.md has the commands.

Proposed fixes, each its own PR with a plan first:

1–4: bind each approval or piece of feedback to the plan current when the message arrived (for Gitea, the latest plan comment before it, since IDs only grow), with gate-qualified revision tags. This mostly implements A4's "only when unambiguous".
5: make publishing adopt an existing PR for the branch instead of failing.
6: record the review comment being worked on, and redeliver it with a notice after a restart.
7: close the plan issue with a note on project complete.

When each fix lands, its scenario's expect flips to the property holding and its xfail comes off.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

A [Quint](https://quint-lang.org) model of `nisse-dev`'s control loop, used to search for counterexamples. **No behaviour changes**: the fixes follow as separate PRs. **The model** (`specs/orchestrator.qnt`, notes in `specs/README.md`) - **Covers** `control.py`'s states, the gate, pending questions, Gitea comment cursors, publish intents and the worker queue. Each pure function is named after the method it mirrors. - **Interleaves freely:** operator messages (every command and free text), comments on the plan issue and the PR, planner/executor/publisher outcomes including exceptions, and **a crash at any point**. Publishing is split into its four steps so a crash can land between them. - **Eight properties.** Each message records the plan the operator had seen when sending it, so the model can tell when an approval lands on the wrong plan. **Results: seven counterexamples.** Each is written out as a short trace in `specs/orchestrator_scenarios.qnt` and **reproduced against the real code** in `nisse-dev/tests/test_quint_counterexamples.py`, marked `xfail(strict=True)` until fixed. Each test was checked to fail on its own assertion, not a harness error. | # | Trace | Real behaviour | |---|---|---| | 1 | "approve" sent twice, both queued | the second approves the milestone plan, never shown | | 2 | "approve rev-1" meant for the architecture | approves milestone-1 rev-1: tags carry no gate name | | 3 | approve in Matrix and on the Gitea issue | the queued Gitea approval approves the next plan | | 4 | "approve" plus an afterthought | the note rejects the milestone plan, which is re-planned | | 5 | crash after the PR opens, before `PR_OPEN` | restart → `continue` → `start` publishes again; Gitea refuses; no way back to `PR_OPEN` | | 6 | crash while answering a review comment | the comment is never answered, and nobody is told | | 7 | `project complete` | the plan issue is left open (`abandon` closes it) | **What held:** `no_stranding`, `await_input_has_a_question` and `execution_needs_approval` over 200,000 random traces of up to 40 steps each, and under Apalache's exhaustive check to depth 8. That depth is shallow, but Apalache does find counterexample 1 within it, so the search is exhaustive at that depth. **Limits:** the model is hand-written from the code. It finds flaws the design and code share, not places where the code strays from the design; that's why each result is also reproduced against the real code. CI doesn't run Quint: it needs Node for the simulator and Java 21 for Apalache. `specs/README.md` has the commands. **Proposed fixes, each its own PR with a plan first:** - **1–4:** bind each approval or piece of feedback to the plan current when the message arrived (for Gitea, the latest plan comment before it, since IDs only grow), with gate-qualified revision tags. This mostly implements A4's "only when unambiguous". - **5:** make publishing adopt an existing PR for the branch instead of failing. - **6:** record the review comment being worked on, and redeliver it with a notice after a restart. - **7:** close the plan issue with a note on `project complete`. When each fix lands, its scenario's `expect` flips to the property holding and its `xfail` comes off. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dev-agent added 1 commit 2026-09-29 18:52:00 +00:00

Model the orchestrator in Quint, and reproduce its counterexamples

CI / checks (push) Skipped

CI / checks (pull_request) Successful in 1m14s

Details

d79e399933

specs/orchestrator.qnt models control.py: states, gate, pending
questions, comment cursors, publish intents and the worker queue, with
operator messages, Gitea comments, work outcomes (exceptions included)
and a crash at any point interleaving freely. Eight properties.

Seven counterexamples, each written out as a trace in
specs/orchestrator_scenarios.qnt and reproduced against the real code in
nisse-dev/tests/test_quint_counterexamples.py (xfail, strict, until
fixed):

1-4 an approval or feedback lands on a plan the operator had not seen:
    a double 'approve', 'approve rev-1' meant for the architecture,
    approving on both channels, and 'approve' plus an afterthought;
5   a crash after the PR opens but before PR_OPEN publishes again and
    cannot get back to PR_OPEN;
6   a crash while answering a review comment loses it silently;
7   'project complete' leaves the plan issue open.

no_stranding, await_input_has_a_question and execution_needs_approval
held over 200,000 random traces of 40 steps, and under Apalache's
exhaustive check to depth 8, which does find counterexample 1 at that
depth. No behaviour changes here.

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

dev-agent added 1 commit 2026-09-29 18:52:07 +00:00

Ignore Apalache's output directory

CI / checks (push) Skipped

CI / checks (pull_request) Successful in 1m18s

Details

9f38e7a467

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

dongar approved these changes

2026-09-29 18:53:08 +00:00

dongar merged commit 6c83839f4d into main

2026-09-29 18:56:30 +00:00

dongar deleted branch quint-orchestrator-spec

2026-09-29 18:56:30 +00:00

dev-agent referenced this pull request

2026-09-29 19:13:21 +00:00

Bind approvals and feedback to the revision they were about #74

dev-agent referenced this pull request

2026-09-29 19:58:20 +00:00

Adopt an already-published PR instead of publishing again #75

dev-agent referenced this pull request

2026-09-29 20:30:32 +00:00

Redeliver an interrupted review comment, and close the issue on completion #76

Sign in to join this conversation.

2 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: dev/nisse#73