End-to-end verification chain: Verus → Rocq → Lean → Kani for all five engines

[avrabe]

Current state

Track 1 (Verus/Z3): ALL 5 engines PASS ✓
Track 2 (Rocq): Not started — needs coq_of_rust on verus-stripped plain Rust
Track 3 (Lean): Not started — scheduler/priority mathematical proofs
Track 4 (Kani): Harnesses written (12 total), not run in CI

What each track proves (and doesn't)

Verus (done)

Proves: functional correctness of each function.

• Bounded output, comparison semantics, persistence logic, invariant preservation.
• Does NOT prove: inter-function properties, system-level composition, timing.

Rocq (needed)

Proves: deeper mathematical properties, refinement between spec and impl.

• Invariant induction across ALL operation sequences (not just individual calls).
• Deadlock freedom when engines are composed.
• Equivalence to a reference cFS specification (behavioral refinement).

Lean (needed)

Proves: scheduling theory, timing, fairness.

• Rate Monotonic schedulability for the Spar AADL model.
• Priority ceiling correctness when engines share resources.
• WCET bounds formalized (connects to relay#2).

Kani (needs CI)

Proves: absence of panics, overflow, UB for bounded state spaces.

• 12 harnesses already written, need cargo kani or Bazel kani_test.
• Covers edge cases Verus specs might miss.

Sequence

1. Run Kani harnesses (lowest effort — harnesses exist)
2. Run coq_of_rust on plain/src/engine.rs → generate Rocq .v files
3. Write Rocq proofs for invariant induction
4. Write Lean proofs for WCET and scheduling
5. Wire all into CI: bazel test //:verus //:kani //:rocq //:lean

Goal

For each engine: 4 independent verification tracks agree.
This is what makes Relay unique — not one proof technique, but four independent ones confirming the same properties.