The README carries a flat green Formally_Verified badge, but rules_verus is Bazel plumbing that wires the Verus SMT verifier (verus_library / verus_test, verus-strip) into downstream builds — it carries no proofs about its own code (a verus! / #[verifier search returns nothing).
The generic badge (a) flattens the specific technique (Verus SMT) into a generic verified-checkmark and (b) reads as if this repo is itself formally verified, when it is a prover-integration layer. Your own sibling rules_lean models the honest label: no flat badge, just "building and verifying Lean 4 libraries and proofs." Suggest a technique-named badge (e.g. Verus-SMT) or wording like "wires the Verus verifier," so the claim matches what the repo does.
🤖 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 a flat green
Formally_Verifiedbadge, but rules_verus is Bazel plumbing that wires the Verus SMT verifier (verus_library/verus_test,verus-strip) into downstream builds — it carries no proofs about its own code (averus!/#[verifiersearch returns nothing).The generic badge (a) flattens the specific technique (Verus SMT) into a generic verified-checkmark and (b) reads as if this repo is itself formally verified, when it is a prover-integration layer. Your own sibling
rules_leanmodels the honest label: no flat badge, just "building and verifying Lean 4 libraries and proofs." Suggest a technique-named badge (e.g.Verus-SMT) or wording like "wires the Verus verifier," so the claim matches what the repo does.🤖 Filed via Claude Code as part of the org-wide verification-claim honesty audit (follows pulseengine/kiln#423). Root: pulseengine/.github#8