v5.0.0 — the fleet study, the Tier 3 replication, and an external benchmark run

polyvers gains an evidence base. The compatibility mechanism was previously argued for; it is now measured — in a pre-registered three-tier fleet study — and replicated against an external benchmark task.

Corpus provenance is decisive

Four incompatible changes, run against corpora differing only in where the states came from:

corpus	caught
archived (real provenance)	4/4
synthesized (BFS-reachable states of the old machine)	3/4

The one that escapes is the landmine: a state the old version could reach, that production therefore holds, and that the new version forbids. A synthesized corpus cannot contain it, because it contains only states the old model says are reachable. Same tool, same change, same gates — the verdict turns on provenance alone. No false positives on either tier.

The composition cases separate the two levels of the cross-machine check: a narrowed cancel window passes the pairwise matrix and fails the joint product.

A machine can be internally consistent and still unsafe to deploy

A dunning-budget narrowing explores 19 states clean from init() and fails seeded from the fleet, which holds a subscription at exactly the depth the new budget makes terminal. Affected population: one snapshot — stated, because class of defect and blast radius are different claims.

Real releases do not announce themselves

Two Medusa version pairs, replayed under a freeze protocol (the old-version model committed before the new version's diff is read):

pair	one-line summary	outcome
v2.4.0 → v2.5.0	"enum gains members"	FAIL — 6 of 32 states stranded
v2.17.1 → v2.17.2	"enum gains a member"	PASS — 0 stranded

Interchangeable summaries, opposite behaviour. The first changed a status derivation; the second changed nothing but a domain. A team classifying either from its release notes would have been wrong in both directions. The first finding is corroborated by the maintainers' own PR text, which names that inconsistency class as deferred work.

Conformance and exploration fail in different directions

An external replication on SysMoBench's etcd Raft task — real traces from a real 3-node cluster, via the tracing hook upstream in etcd-io/raft:

	replay	explorer + invariants
8 injected defects	2/8	1/8 definitive, 6/8 inconclusive
5 one-shot generated specs	4/5	0/5

Replay misses defensive code a correct system never drives — including the heartbeat clamp this project's own prior work singles out. The explorer misses anything the stated invariants omit. Neither subsumes the other, and a specification graded by either alone gets a clean bill it has not earned.

⚠️ Commit f6743a7's title reports "the explorer catches 8/8". That figure is wrong — it was a regex matching the word "violations" inside no invariant violations reachable, and was corrected in 59345b6. The table above is authoritative.

What it reports against itself

• A projection-bound miss. A zero-amount payment collection reads unpaid under one version and completed under the next; the declared money abstraction collapses at zero, so the case is inexpressible. Out-of-projection, with the bound declared before the analysis.
• A self-inflicted false positive. Rewording type-description prose manufactured a shape diff — operator error, reported rather than quietly fixed.
• Two measurement bugs, both caught by control rows deliberately scored on identical terms.
• A corrected claim in the paper. Finite action domains do not imply a finite state space: exhaustiveness requires a finite reachable state space, which a contract is not currently required to declare.

Also in this release

Two polyvers defects the study found and fixed: the migrate gate conflating structural with invariant failures, and the semantic gate understating its own coverage. Plus polyrun simulate, the joint product check, engine READMEs rewritten as introductions, and the SDLC diagrams.

Bounded results are not passes — enforced in code throughout, not assumed.