buzz/docs/spec at eva/redis-cluster-mode-spec - buzz

mirror of https://github.com/block/buzz.git synced 2026-08-18 06:50:31 +02:00

Files

T

History

npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d 56303ba8ea docs: drain-reachability probe (M10) + B->A rollback session-loss note

Review round 2 (Dawn) found the safety model could not distinguish the
B2 fix from its absence: unguarded ExpireOld lets the C-gate be
discharged by luck, so deleting MigrateB left all invariants green.
Added DrainSpec/Probe_NotC — TLC from the stall state (full-B fleet, live
old-key lease, no spontaneous expiry) with inverted verdict semantics:
violation proves C reachable (93/44); mutant M10 (MigrateB removed =
round-1 behavior) stays green, making the round-1 bug permanently
visible. Main safety model unchanged (12636/3637, M1-M9 all killed).

Also per Dawn N1: rollback matrix now names B->A as dropping every
migrated session (A renews the old key; nobody renews the migrated
lease; renewer treats Lost as fatal) — liveness cost, prefer forward-fix.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

2026-07-30 12:10:28 -04:00

.gitignore

Multi-tenant relay: spec + mechanized formal proof (S1–S8) (#1285 )

2026-06-26 11:15:59 -04:00

GitOnObjectStore.cfg

docs: formal spec + machine-checked proof for git refs over object storage (#721 )

2026-05-21 23:43:46 -04:00

GitOnObjectStore.tla

perf(relay): compact Git packs before manifest limits (#2172 )

2026-07-20 19:36:28 +02:00

MultiTenantAuth.spthy

Multi-tenant relay: spec + mechanized formal proof (S1–S8) (#1285 )