Sync Formal Modeling - P & Occult - #1115

Closed

kans wants to merge 27 commits into

mainfrom

kans/sync-formal-model

Commits on Aug 28, 2026

sync: source-cache replay orchestration (phase 6b)

kans
and
cursoragent
committed
c33f698
Round-4 review remediation (CO-6b-007): held-lock ride-along, coverage triage, witness pin

kans
and
cursoragent
committed
909375d

Commits on Aug 31, 2026

formal: sync scheduling models — P calibration + Occult deductive track

kans
and
cursoragent
committed
e4e0e9c
formal/graph: bake-off phase complete — verdict is variant S (BAKEOFF.md)

kans
and
cursoragent
committed
4b06475
formal/occult: close the trace bridge against the shipped syncer

kans
and
cursoragent
committed
f610d26
formal/occult: multi-attempt traces — ev_resume extension + a resume-path finding

kans
and
cursoragent
committed
a730b01
formal/occult: tombstone delete leg in the trace-policy oracle

kans
and
cursoragent
committed
ad611a7
formal: synthesis report (REPORT.md)

kans
and
cursoragent
committed
eff4b6d
docs: RFC 0011 kickoff — demand-graph sync runtime (variant S)

kans
and
cursoragent
committed
f7b6db0
formal/walker: drop machine-replay trace archives from the repo

kans
and
cursoragent
committed
21a3193
pkg/sync: fix the phantom union on the verdict-flip path (record-round grounding)

kans
and
cursoragent
committed
30f4f1b
pkg/sync: sessions are attempt-scoped under the source-cache protocol (CO-6b-009)

kans
and
cursoragent
committed
ab99c65
formal/occult: pin constrained-universal dispatch semantics; lint hygiene

kans
and
cursoragent
committed
f0ae52b
pkg/sync: revert session resume-clear; pin persistence semantics (CO-6b-009)

kans
and
cursoragent
committed
7e70c69
formal: capture session-checkpoint consistency in both systems (CO-6b-009)

kans
and
cursoragent
committed
e2e31e0
formal: model external principals in both systems (scenario 8 / policy 7)

kans
and
cursoragent
committed
b9fdf6e
formal/walker: drop per-cell counterexample archives; regenerate on demand

kans
and
cursoragent
committed
85ad8a6
formal: address PR 1117 review round 1

kans
and
cursoragent
committed
bd6339e
formal: disposition round-2 findings (independent model reviews)

kans
and
cursoragent
committed
e3de22f
formal: add make targets for the model sweeps and Occult suite

kans
and
cursoragent
committed
85e266c
formal: restore the bake-off alarm audit, drop a dead probe fixture

kans
and
cursoragent
committed
9fc750a
formal: make the verdict scripts' exit status carry the verdict

kans
and
cursoragent
committed
732f5fb

Commits on Sep 1, 2026

formal: round-4 review batch + full-pass validation

kans
and
cursoragent
committed
77b0b2f
formal: complete the walker run log's missing scenario-4 section

kans
and
cursoragent
committed
dc8eab8
formal: close the residual grammar-guard gaps in the verdict scripts

kans
and
cursoragent
committed
240be1c
formal: witness P8's over-deletion clause, guard LoadExpressions, register unwitnessed-clause inventory

kans
and
cursoragent
committed
a569b49
formal: walker log carries its own coverage limit; tc3a_P1 row states the two-shape contract

kans
and
cursoragent
committed
f853dae