Part of the V&V coverage initiative.
Problem
relay has rich V&V content — 25 Bazel test targets, Rocq proofs in proofs/rocq/, Lean proofs in proofs/lean/ (BackpressureSafety, WcetAnalysis, CompositionalWcet), fuzz targets in fuzz/fuzz_targets/, differential testing in crates/relay-lc-diff/ — but zero .github/workflows/. Everything runs locally only.
Acceptance
Notes
- Rocq toolchain from rules_rocq_rust (Nix-hermetic); mirror meld's CI
- Lean toolchain from rules_lean, pin 4.27.0
- Keep engines (LC/SCH/SC/HS/CFDP) as separate bench/fuzz groups for targeted regression
Part of the V&V coverage initiative.
Problem
relay has rich V&V content — 25 Bazel test targets, Rocq proofs in
proofs/rocq/, Lean proofs inproofs/lean/(BackpressureSafety, WcetAnalysis, CompositionalWcet), fuzz targets infuzz/fuzz_targets/, differential testing incrates/relay-lc-diff/— but zero.github/workflows/. Everything runs locally only.Acceptance
.github/workflows/ci.ymlon PR + main:bazel test //...bazel test //proofs/rocq/...and//proofs/lean/...rivet validate.github/workflows/nightly.yml: long-fuzz runs (1h per target)Notes