Repository navigation
4 pre-existing Alloy model violations exposed by the #199 detector fix #218
Description
Summary
PR #214 (issue #199) fixed the Alloy runners so they actually detect assertion violations. That fix immediately surfaced 4 genuine, pre-existing formal-model violations that the dead /Counterexample/i regex had been silently recording as pass. These are NOT regressions introduced by #214 — they exist on main today and have been reported green the whole time.
The 4 violated specs (from the FV CI run on #214)
| Check | Spec | Evidence |
|---|---|---|
alloy:quorum-composition |
.planning/formal/alloy/quorum-composition.als |
check AllRulesHold → counterexample (skolem $AllRulesHold_c={Config$0}); reproduced with Alloy 6.2.0 |
alloy:install-scope |
install-scope.als |
Alloy verification FAILED with instance block |
alloy:taxonomy-safety |
taxonomy-safety.als |
Alloy verification FAILED with instance block |
alloy:transcript-scan |
transcript-scan.als |
TraceDivergenceDetected counterexample (skolem $TraceDivergenceDetected_tc) |
All 4 report assertion counterexamples (not vacuity / not parser errors — the new parser's 18 existing runner tests stay green).
Why this matters
This is the core risk that issue #199 was about: the formal-verification surface could not report a violation, so 4 genuinely-violated invariants were being counted as verified. Each needs triage:
- Real system bug — the modeled behavior is wrong → fix the implementation.
- Wrong assertion — the spec over-constrains → fix the
.als. - Stale model — the spec drifted from the current design → update or retire it.
Action
- Triage
quorum-compositionAllRulesHold(start here — confirmed real counterexample) - Triage
install-scope - Triage
taxonomy-safety - Triage
transcript-scanTraceDivergenceDetected - Decide CI policy for fix(formal): detect Alloy 6 counterexamples via receipt.json, not dead regex (#199) #214: waive these 4 as known-failing (ratchet) so the detector lands and guards NEW specs, or hold fix(formal): detect Alloy 6 counterexamples via receipt.json, not dead regex (#199) #214 until they're fixed.
Blocks/relates to #214 (#199). Part of the 2026-06 quorum-hardening series.
Activity
jobordu commentedon Jun 19, 2026
Deep assessment complete — all 4 are SPEC bugs, none are implementation bugs
Each violation was reproduced with Alloy 6 and cross-referenced against the implementation. The code is correct in every case; the models were wrong, and the dead
/Counterexample/iregex hid it. Being fixed in PR #214 (spec-only, no waivers):quorum-composition / AllRulesHoldHigh ⇒ ≥1 slotunconditionally; facts only guarantee that when#availableSlots > 0. Empty/all-down roster is the counterexample — real system routes it to solo mode.#availableSlots > 0guard so the assertion matches the facts.install-scope / AllEquivalence--all --globalvs--all --local).InstallOpat one fixed scope (mirrors the passingInstallIdempotent).taxonomy-safety / TaxonomyClosed + NewCategoryConsistentClassificationto the snapshot it was classified against, so the solver picks mismatched pairs.Classification.againstto its snapshot + model theis_newclassifier contract as a fact. Also: stale provenance —SCBD-05/06/07referenced but absent from requirements.json.transcript-scan / PairingUniqueChecktool_use/tool_resultIDs, so the solver collapses many onto one Id atom.block.id).transcript-scan / SuccessCountNeverExceedsMinSizeChecksuccessCountbyminSizeper a removedqgsd-stop.js:453break; current code breaks atsuccessCount >= maxSize(nf-stop.js:1069) since the #192 min_live_voters rework.maxSize, update source-line comments.Net: no implementation changes needed. Once #214's spec fixes land green, this issue is resolved (modulo the separate cleanup of the missing SCBD-05/06/07 requirement entries, which I'll leave noted here).
jobordu commentedon Jun 19, 2026
The 4 Alloy specs are fixed and merged via #214 (#199) — all spec/model bugs, no implementation changes. Formal CI is green. Leaving this issue open only for the residual cleanup: create the missing
SCBD-05/06/07requirement entries in.planning/formal/requirements.json(referenced by the taxonomy-safety spec's @requirement tags).