feat: bootstrap rivet verification scaffolding, seed hazard analysis for #37

[avrabe]

Summary

• rules_rocq_rust had no rivet project. This initializes one (stpa + dev schemas) and seeds the top of the V so Toolchain: add Flocq + Gappa + Coq-Interval to enable machine-checked floating-point error-bound proofs #37 (add Flocq/Gappa/Coq-Interval for machine-checked FP error-bound proofs) can be driven through the feature loop with traceability from commit one.
• STPA: the loss is a false "verified" signal from this toolchain propagating into a downstream safety case (e.g. relay's flight-math kernels). H-001 generalizes an already-fixed failure class (the smpl .vo version mismatch in PR chore: upgrade Rocq 9.0 → 9.1 #30, the rocq_library -Q path issue in fix(rocq_library): add self -Q even when out_dir is parent of dep paths #35). H-002 is the new risk Toolchain: add Flocq + Gappa + Coq-Interval to enable machine-checked floating-point error-bound proofs #37 introduces: trusting a Gappa-emitted proof certificate without replaying it through the Rocq kernel.
• REQ-001/DD-002 document the existing mechanism (Bazel action-failure semantics + explicit Rocq-version pinning) that already satisfies the general constraint.
• REQ-002/DD-001/FEAT-001 capture Toolchain: add Flocq + Gappa + Coq-Interval to enable machine-checked floating-point error-bound proofs #37's own technical assessment (Gappa for rounding, Coq-Interval for approximation, Flocq underneath, every Gappa certificate kernel-replayed) as the accepted design.

Test plan

• rivet validate passes (0 errors, 1 expected warning class — no test artifacts yet, this is the scaffold not the implementation)

Relates to #37

🤖 Generated with Claude Code

https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey