spar is a compiler/generator (AADL/SysML/CAN-DBC → WIT/Rust/Lean/rivet), which makes it the most natural fit for the generation-over-checking approach — and it already proves the strongest kind of spec: external published theory (Liu & Layland, Joseph & Pandya, Dertouzos, Feiertag), so the ground truth isn't a self-authored mirror.
The drift point is the theory↔code link: proofs/Codegen.lean labels the Lean→Rust step a 'manual extraction', and RTAJittered.lean says 'the Rust implementation is checked against this spec via property tests'. So today the Lean proves the math and property tests guard a hand extraction to the Rust that computes it.
Approach move (pure single-source): generate the Rust analysis code from the same definition the Lean proofs are stated over (spar already generates code — point that machinery at the scheduling/min-plus core), so 'the Rust implements the proven theory' becomes a generated property, not a manually-extracted one checked after the fact. Property tests then verify the generator, once, instead of every extraction. That retires the manual-extraction line from the trusted base.
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).
spar is a compiler/generator (AADL/SysML/CAN-DBC → WIT/Rust/Lean/rivet), which makes it the most natural fit for the generation-over-checking approach — and it already proves the strongest kind of spec: external published theory (Liu & Layland, Joseph & Pandya, Dertouzos, Feiertag), so the ground truth isn't a self-authored mirror.
The drift point is the theory↔code link:
proofs/Codegen.leanlabels the Lean→Rust step a 'manual extraction', andRTAJittered.leansays 'the Rust implementation is checked against this spec via property tests'. So today the Lean proves the math and property tests guard a hand extraction to the Rust that computes it.Approach move (pure single-source): generate the Rust analysis code from the same definition the Lean proofs are stated over (spar already generates code — point that machinery at the scheduling/min-plus core), so 'the Rust implements the proven theory' becomes a generated property, not a manually-extracted one checked after the fact. Property tests then verify the generator, once, instead of every extraction. That retires the manual-extraction line from the trusted base.
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).