Certora round 3: refresh drifted specs, conservation slices, CI gate#42

Merged

Noc2 merged 12 commits into

mainfrom

certora-followup-research-3

Jun 9, 2026

Commits on Jun 9, 2026

docs(certora): round-3 plan — narrowed, research-backed next steps

Noc2
and
claude
committed
test(certora): refresh oracle spec for new rejection branches

Noc2
and
claude
committed
test(certora): Track C aggregate-conservation slice + mul-div lemma

Noc2
and
claude
committed
ci(certora): add secret-free type-check gate + spec-freshness guard (Track G)

Noc2
and
claude
committed
test(certora): wire up Gambit mutation testing (spec-strength check)

Noc2
and
claude
committed
test(certora): machine-check the launch cap-assignment clamp (Track B)

Noc2
and
claude
committed
ci(certora): QRPE timeout load-cut + correct the resolver finding (Track D)

Noc2
and
claude
committed
docs(certora): Track A escalation write-up + round-3 status sync

Noc2
and
claude
committed
fix(certora): track transitive library imports in spec-freshness guard

Noc2
and
claude
committed
ci(certora): use the runner's preinstalled JDK 21 for the type-check gate

Noc2
and
claude
committed
test(certora): drop artifact-tripping frontend dust rule (cloud-prover fix)

Noc2
and
claude
committed
style(foundry): forge fmt ClusterPayoutOracle.sol + test flagged by CI lint

Noc2
and
claude
committed