dev/nisse
2
1 Fork 0
Code Issues 23 Pull Requests 1 Actions Packages Projects Releases 1 Wiki Activity
241 Commits 3 Branches 1 Tag
v0.1.0
Commit Graph
3 Commits
Author SHA1 Message Date
dongarandClaude Opus 5.5 266b5dbbd7 Check loop.qnt's properties against the real loop (M2.1, PR D part 1)
CI / checks (push) Skipped 
test_loop_properties.py walks the new loop with a seeded mix of operator
and Gitea actions (go-aheads, stale go-aheads, answers, comments, merges,
the comment-then-merge race, closes, abandon, a crash and restart) and an
adaptive scripted model, checking every loop.qnt property after every
step. It found two bugs, both fixed with regression tests: abandoning an
item left its open PR open (the model's fix 1, now in code), and after a
review fix became a follow-up PR, the next fix went to the merged branch.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
 2026-10-03 14:19:19 +00:00
dongarandClaude Opus 5.5 76e9fa38c7 Model the agent loop as the architecture describes it
CI / checks (push) Skipped
CI / checks (pull_request) Successful in 1m24s
Details 
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
 2026-10-02 19:24:39 +00:00
dongarandClaude Opus 5.5 d79e399933 Model the orchestrator in Quint, and reproduce its counterexamples
CI / checks (push) Skipped
CI / checks (pull_request) Successful in 1m14s
Details 
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
 2026-09-29 18:51:59 +00:00