The README carries the flat green Formally_Verified badge, but rules_rocq_rust is Bazel/Nix plumbing that wires Rocq 9.0 + rocq-of-rust into builds; the only .v proof in the tree is examples/rust_to_rocq/point_proofs.v (an example) — the repo carries no mechanized proofs about its own rules.
The generic badge both flattens the specific technique (Rocq theorem proving) and reads as if the repo itself is verified. Sibling rules_lean already models the honest label (no flat badge). Suggest a technique-named badge (e.g. Rocq).
🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows pulseengine/kiln#423). Root: pulseengine/.github#8
The README carries the flat green
Formally_Verifiedbadge, but rules_rocq_rust is Bazel/Nix plumbing that wires Rocq 9.0 + rocq-of-rust into builds; the only.vproof in the tree isexamples/rust_to_rocq/point_proofs.v(an example) — the repo carries no mechanized proofs about its own rules.The generic badge both flattens the specific technique (Rocq theorem proving) and reads as if the repo itself is verified. Sibling
rules_leanalready models the honest label (no flat badge). Suggest a technique-named badge (e.g.Rocq).🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows pulseengine/kiln#423). Root: pulseengine/.github#8