Model the agent loop as the architecture describes it #91

2026-10-02T19:25:16Z

dev-agent commented

2026-10-02 19:25:16 +00:00

A Quint model of the agent loop as docs/Architecture.md describes it in #90. The new loop doesn't exist yet, so a counterexample here is a gap in the architecture, fixed there. The fixes are on #90 (commit 8c38444), and the model carries them (marked FIX n).

orchestrator.qnt is unchanged; it still guards control.py until that's retired.

What it models

Work items from assigned issues and from conversations, with record issues.
Restatements, and go-aheads bound to the revision on screen.
Bug grace periods.
Park-and-switch, with branches pushed on parking.
Blocked dependencies.
start_milestone / finish_milestone, with publish intents.
Waiting for merges; PRs merged, closed or commented on.
Review follow-ups.
Abandon.
Crashes at any point, lost Gitea responses, and build VM wipes.

Properties

Property	Meaning
`one_item_per_issue`	An issue is the record of at most one work item
`waits_are_explainable`	Every wait is for something the operator can see, or a recorded dependency (L2)
`go_binds`	Work starts only on a go-ahead for the revision the operator saw (L3)
`milestone_after_merge`	The next milestone starts only after the previous PR merged (D4)
`parked_work_safe`	A parked item's unpushed work is never set aside or wiped
`one_pr_per_milestone`	Never two PRs for one milestone
`review_fixes_land`	A review fix always reaches an open PR
`closed_items_leave_nothing`	A closed item leaves no open PR or pending intent

What it found

Five gaps, each now fixed in #90 and kept as a regression trace in loop_scenarios.qnt:

Abandon left the item's open PR open. L2 now closes it.
A retry reopened a PR the operator had closed. Gitea opened the PR, but the response was lost; you then closed it, and the retry, which only adopted open PRs, opened a second one. A closed PR is now an answer (L8).
A review fix could land on a PR that had already merged, and so never reach main. After pushing a fix, the agent now checks the PR; if it merged meanwhile, the fix goes out as a new PR (D5).
After a closed PR, the next milestone could start with the closed one never merged. A redo is now the same milestone on a new branch (D4).
Intake could take a record issue for new work in the moment between the agent opening it and storing the link. The issue now carries its work item's ID from creation (D1).

How it was checked

Random simulation: about 200k traces of 80 steps, clean on all properties with the fixes in.
The w_* reachability witnesses confirm the deep states are reached: second milestones, merges, reviews, blocked items and finished items.
Each trace fails with its fix reverted. Each property that never failed (go_binds, parked_work_safe, waits_are_explainable) was checked against a deliberately broken model, and caught it.
Bounded exhaustive check: quint verify to depth 6. The result will be posted as a comment.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

A Quint model of the agent loop **as `docs/Architecture.md` describes it in #90**. The new loop doesn't exist yet, so a counterexample here is a gap in the architecture, fixed there. The fixes are on #90 (commit `8c38444`), and the model carries them (marked `FIX n`). `orchestrator.qnt` is unchanged; it still guards `control.py` until that's retired. ## What it models - Work items from assigned issues and from conversations, with record issues. - Restatements, and go-aheads bound to the revision on screen. - Bug grace periods. - Park-and-switch, with branches pushed on parking. - Blocked dependencies. - `start_milestone` / `finish_milestone`, with publish intents. - Waiting for merges; PRs merged, closed or commented on. - Review follow-ups. - Abandon. - Crashes at any point, lost Gitea responses, and build VM wipes. ## Properties | Property | Meaning | |---|---| | `one_item_per_issue` | An issue is the record of at most one work item | | `waits_are_explainable` | Every wait is for something the operator can see, or a recorded dependency (L2) | | `go_binds` | Work starts only on a go-ahead for the revision the operator saw (L3) | | `milestone_after_merge` | The next milestone starts only after the previous PR merged (D4) | | `parked_work_safe` | A parked item's unpushed work is never set aside or wiped | | `one_pr_per_milestone` | Never two PRs for one milestone | | `review_fixes_land` | A review fix always reaches an open PR | | `closed_items_leave_nothing` | A closed item leaves no open PR or pending intent | ## What it found Five gaps, each now fixed in #90 and kept as a regression trace in `loop_scenarios.qnt`: 1. **Abandon left the item's open PR open.** L2 now closes it. 2. **A retry reopened a PR the operator had closed.** Gitea opened the PR, but the response was lost; you then closed it, and the retry, which only adopted *open* PRs, opened a second one. A closed PR is now an answer (L8). 3. **A review fix could land on a PR that had already merged,** and so never reach main. After pushing a fix, the agent now checks the PR; if it merged meanwhile, the fix goes out as a new PR (D5). 4. **After a closed PR, the next milestone could start** with the closed one never merged. A redo is now the same milestone on a new branch (D4). 5. **Intake could take a record issue for new work** in the moment between the agent opening it and storing the link. The issue now carries its work item's ID from creation (D1). ## How it was checked - **Random simulation:** about 200k traces of 80 steps, clean on all properties with the fixes in. - **The `w_*` reachability witnesses confirm the deep states are reached:** second milestones, merges, reviews, blocked items and finished items. - **Each trace fails with its fix reverted.** Each property that never failed (`go_binds`, `parked_work_safe`, `waits_are_explainable`) was checked against a deliberately broken model, and caught it. - **Bounded exhaustive check:** `quint verify` to depth 6. The result will be posted as a comment. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dev-agent added 1 commit 2026-10-02 19:25:17 +00:00

Model the agent loop as the architecture describes it

CI / checks (push) Skipped

CI / checks (pull_request) Successful in 1m24s

Details

76e9fa38c7

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

dev-agent commented

2026-10-02 19:26:17 +00:00

Bounded exhaustive check finished: quint verify specs/loop.qnt --invariant=all_properties --max-steps=6 reports no violation (Apalache, about 3.5 minutes). Depth 6 is shallow: no PR can open in 6 steps from init, so this covers intake, restatement, go-ahead binding and parking. The deep paths are covered by random simulation, as noted in the PR description.

🤖 Generated with Claude Code

Bounded exhaustive check finished: `quint verify specs/loop.qnt --invariant=all_properties --max-steps=6` reports **no violation** (Apalache, about 3.5 minutes). Depth 6 is shallow: no PR can open in 6 steps from init, so this covers intake, restatement, go-ahead binding and parking. The deep paths are covered by random simulation, as noted in the PR description. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dongar approved these changes

2026-10-02 19:36:19 +00:00

dev-agent merged commit b7f1f3371c into main

2026-10-02 19:36:45 +00:00

dev-agent deleted branch loop-model

2026-10-02 19:36:45 +00:00

Sign in to join this conversation.

2 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: dev/nisse#91