gale has genuinely independent backends (Verus/Z3, Lean/Mathlib, Rocq-kernel) — but two approach upgrades sharpen it:
- Use the two Rocq styles adversarially. The behavioural Rocq proofs run over
coq_of_rust-translated code (bzl/private/verus_to_rocq.bzl — derived from the same Verus source), while the abstract-Z proofs are hand-written and independent. Right now they largely partition properties. The bug-finding move: where the hand-written abstract model and the translated-code proof both speak to the same invariant, run them against each other and treat a disagreement as a found spec/translation bug — the way two independent mechanisations of a spec surface its ambiguities. A model derived from the code + a model written against intent, cross-checked, catches the drift neither catches alone.
- Promote
cargo-mutants from nightly to per-PR. Mutation is the meta-oracle that catches a proof passing because its spec is vacuous — and it currently runs only in the nightly suite, exactly where a vacuous-spec regression can slip in undetected for a day.
The POSIX/FreeRTOS differential_spec.rs is already the reference-oracle move done right — keep leaning on it.
Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).
gale has genuinely independent backends (Verus/Z3, Lean/Mathlib, Rocq-kernel) — but two approach upgrades sharpen it:
coq_of_rust-translated code (bzl/private/verus_to_rocq.bzl— derived from the same Verus source), while the abstract-Z proofs are hand-written and independent. Right now they largely partition properties. The bug-finding move: where the hand-written abstract model and the translated-code proof both speak to the same invariant, run them against each other and treat a disagreement as a found spec/translation bug — the way two independent mechanisations of a spec surface its ambiguities. A model derived from the code + a model written against intent, cross-checked, catches the drift neither catches alone.cargo-mutantsfrom nightly to per-PR. Mutation is the meta-oracle that catches a proof passing because its spec is vacuous — and it currently runs only in the nightly suite, exactly where a vacuous-spec regression can slip in undetected for a day.The POSIX/FreeRTOS
differential_spec.rsis already the reference-oracle move done right — keep leaning on it.Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).