@@ -711,12 +711,17 @@ fn count_matching(findings: &[FindingLite], cov: &Coverage) -> usize {
     findings.iter().filter(|f| matches_coverage(f, cov)).count()
 }
 
+/// Return whether a finding falls within the declared coverage, ignoring its claim.
+///
+/// Category names and canonical rule IDs match case-insensitively, ignoring
+/// non-alphanumeric characters. File coverage uses a case-sensitive substring
+/// match against the finding's file text before the first `:`; an empty value
+/// matches any present file. File coverage without file text and free-form
+/// coverage never match.
 fn matches_coverage(f: &FindingLite, cov: &Coverage) -> bool {
     match cov.kind {
         CoverageKind::Category => eq_loose(&category_name(&f.category), &cov.value),
-        CoverageKind::RuleId => category_code(&f.category)
-            .map(|c| eq_loose(c, &cov.value))
-            .unwrap_or(false),
+        CoverageKind::RuleId => eq_loose(f.category.rule_id(), &cov.value),
         CoverageKind::File => f
             .file
             .as_deref()
@@ -816,27 +821,6 @@ fn category_name(c: &WeakPointCategory) -> String {
 }
 
 /// Map a category to its documented PA rule-id where one is assigned.
-fn category_code(c: &WeakPointCategory) -> Option<&'static str> {
-    use WeakPointCategory::*;
-    Some(match c {
-        UnsafeCode => "PA001",
-        PanicPath => "PA006",
-        CommandInjection => "PA011",
-        UnsafeDeserialization => "PA012",
-        DynamicCodeExecution => "PA013",
-        UnsafeFFI => "PA014",
-        AtomExhaustion => "PA015",
-        PathTraversal => "PA017",
-        HardcodedSecret => "PA018",
-        ProofDrift => "PA021",
-        CryptoMisuse => "PA022",
-        SupplyChain => "PA023",
-        InputBoundary => "PA024",
-        MutationGap => "PA025",
-        _ => return None,
-    })
-}
-
 fn read_text_bounded(path: &Path) -> Result<String> {
     let mut buf = String::new();
     File::open(path)
@@ -1015,4 +999,31 @@ mod tests {
         );
         assert_eq!(report.reconciliations[0].affected_findings, 1);
     }
+
+    /// `rule:` coverage reads the same table SARIF emits, for every category.
+    /// Before the table was unified, `rule:PA004` never matched UnsafeCode
+    /// (aggregate called it PA001) and 16 categories had no rule ID at all.
+    #[test]
+    fn rule_coverage_uses_the_canonical_table() {
+        for c in WeakPointCategory::ALL {
+            let f = FindingLite {
+                category: c,
+                file: None,
+            };
+            let own = parse_coverage_spec(&format!("rule:{}", c.rule_id())).unwrap();
+            assert!(
+                matches_coverage(&f, &own),
+                "{c:?} not covered by its own ID"
+            );
+            assert_eq!(c.rule_id(), crate::report::sarif::rule_id(&c));
+        }
+        let unsafe_code = FindingLite {
+            category: WeakPointCategory::UnsafeCode,
+            file: None,
+        };
+        let pa004 = parse_coverage_spec("sound:rule:PA004").unwrap();
+        let pa001 = parse_coverage_spec("sound:rule:PA001").unwrap();
+        assert!(matches_coverage(&unsafe_code, &pa004));
+        assert!(!matches_coverage(&unsafe_code, &pa001));
+    }
 }
@@ -112,40 +112,11 @@ pub struct SarifRegion {
     pub start_line: u32,
 }
 
-/// Map WeakPointCategory to a stable rule ID
+/// Map WeakPointCategory to its stable rule ID. Delegates to the single
+/// table on the enum (`WeakPointCategory::rule_id`) so SARIF, storage and
+/// proof coverage cannot drift apart.
 pub(crate) fn rule_id(category: &WeakPointCategory) -> &'static str {
-    match category {
-        WeakPointCategory::UncheckedAllocation => "PA001",
-        WeakPointCategory::UnboundedAllocation => "PA001b",
-        WeakPointCategory::UnboundedLoop => "PA002",
-        WeakPointCategory::BlockingIO => "PA003",
-        WeakPointCategory::UnsafeCode => "PA004",
-        WeakPointCategory::PanicPath => "PA005",
-        WeakPointCategory::RaceCondition => "PA006",
-        WeakPointCategory::DeadlockPotential => "PA007",
-        WeakPointCategory::ResourceLeak => "PA008",
-        WeakPointCategory::CommandInjection => "PA009",
-        WeakPointCategory::UnsafeDeserialization => "PA010",
-        WeakPointCategory::DynamicCodeExecution => "PA011",
-        WeakPointCategory::UnsafeFFI => "PA012",
-        WeakPointCategory::AtomExhaustion => "PA013",
-        WeakPointCategory::InsecureProtocol => "PA014",
-        WeakPointCategory::ExcessivePermissions => "PA015",
-        WeakPointCategory::PathTraversal => "PA016",
-        WeakPointCategory::HardcodedSecret => "PA017",
-        WeakPointCategory::UncheckedError => "PA018",
-        WeakPointCategory::InfiniteRecursion => "PA019",
-        WeakPointCategory::UnsafeTypeCoercion => "PA020",
-        WeakPointCategory::ProofDrift => "PA021",
-        WeakPointCategory::CryptoMisuse => "PA022",
-        WeakPointCategory::SupplyChain => "PA023",
-        WeakPointCategory::InputBoundary => "PA024",
-        WeakPointCategory::MutationGap => "PA025",
-        WeakPointCategory::LicensePolicy => "PA026",
-        WeakPointCategory::Advisory => "PA027",
-        WeakPointCategory::BannedDep => "PA028",
-        WeakPointCategory::UnknownSource => "PA029",
-    }
+    category.rule_id()
 }
 
 /// Map WeakPointCategory to a human-readable name
 
@@ -447,6 +447,85 @@ pub enum WeakPointCategory {
     UnknownSource,
 }
 
+impl WeakPointCategory {
+    /// Every category, in rule-ID order: the list the consistency tests
+    /// iterate over, and the public enumeration for library consumers.
+    // The binary re-declares this module and never reads ALL itself.
+    #[allow(dead_code)]
+    pub const ALL: [WeakPointCategory; 30] = [
+        WeakPointCategory::UncheckedAllocation,
+        WeakPointCategory::UnboundedAllocation,
+        WeakPointCategory::UnboundedLoop,
+        WeakPointCategory::BlockingIO,
+        WeakPointCategory::UnsafeCode,
+        WeakPointCategory::PanicPath,
+        WeakPointCategory::RaceCondition,
+        WeakPointCategory::DeadlockPotential,
+        WeakPointCategory::ResourceLeak,
+        WeakPointCategory::CommandInjection,
+        WeakPointCategory::UnsafeDeserialization,
+        WeakPointCategory::DynamicCodeExecution,
+        WeakPointCategory::UnsafeFFI,
+        WeakPointCategory::AtomExhaustion,
+        WeakPointCategory::InsecureProtocol,
+        WeakPointCategory::ExcessivePermissions,
+        WeakPointCategory::PathTraversal,
+        WeakPointCategory::HardcodedSecret,
+        WeakPointCategory::UncheckedError,
+        WeakPointCategory::InfiniteRecursion,
+        WeakPointCategory::UnsafeTypeCoercion,
+        WeakPointCategory::ProofDrift,
+        WeakPointCategory::CryptoMisuse,
+        WeakPointCategory::SupplyChain,
+        WeakPointCategory::InputBoundary,
+        WeakPointCategory::MutationGap,
+        WeakPointCategory::LicensePolicy,
+        WeakPointCategory::Advisory,
+        WeakPointCategory::BannedDep,
+        WeakPointCategory::UnknownSource,
+    ];
+
+    /// The canonical, stable rule ID for this category: the one table every
+    /// consumer reads (SARIF `ruleId`, VeriSimDB hexads, the query DSL,
+    /// proof coverage `rule:` annotations, the verdict grid). IDs are a
+    /// public contract: never renumber an existing category; a new category
+    /// takes a new ID. `rule_id_tests::rule_ids_are_stable` locks the table.
+    pub const fn rule_id(self) -> &'static str {
+        match self {
+            WeakPointCategory::UncheckedAllocation => "PA001",
+            WeakPointCategory::UnboundedAllocation => "PA001b",
+            WeakPointCategory::UnboundedLoop => "PA002",
+            WeakPointCategory::BlockingIO => "PA003",
+            WeakPointCategory::UnsafeCode => "PA004",
+            WeakPointCategory::PanicPath => "PA005",
+            WeakPointCategory::RaceCondition => "PA006",
+            WeakPointCategory::DeadlockPotential => "PA007",
+            WeakPointCategory::ResourceLeak => "PA008",
+            WeakPointCategory::CommandInjection => "PA009",
+            WeakPointCategory::UnsafeDeserialization => "PA010",
+            WeakPointCategory::DynamicCodeExecution => "PA011",
+            WeakPointCategory::UnsafeFFI => "PA012",
+            WeakPointCategory::AtomExhaustion => "PA013",
+            WeakPointCategory::InsecureProtocol => "PA014",
+            WeakPointCategory::ExcessivePermissions => "PA015",
+            WeakPointCategory::PathTraversal => "PA016",
+            WeakPointCategory::HardcodedSecret => "PA017",
+            WeakPointCategory::UncheckedError => "PA018",
+            WeakPointCategory::InfiniteRecursion => "PA019",
+            WeakPointCategory::UnsafeTypeCoercion => "PA020",
+            WeakPointCategory::ProofDrift => "PA021",
+            WeakPointCategory::CryptoMisuse => "PA022",
+            WeakPointCategory::SupplyChain => "PA023",
+            WeakPointCategory::InputBoundary => "PA024",
+            WeakPointCategory::MutationGap => "PA025",
+            WeakPointCategory::LicensePolicy => "PA026",
+            WeakPointCategory::Advisory => "PA027",
+            WeakPointCategory::BannedDep => "PA028",
+            WeakPointCategory::UnknownSource => "PA029",
+        }
+    }
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
 pub enum Severity {
     Low,
@@ -959,3 +1038,78 @@ pub enum Predicate {
     },
     Fact(Fact),
 }
+
+#[cfg(test)]
+mod rule_id_tests {
+    use super::WeakPointCategory;
+    use std::collections::HashSet;
+
+    /// Exhaustive by construction: adding a variant without a position here
+    /// is a compile error, which is the prompt to add it to `ALL` as well.
+    fn ordinal(c: WeakPointCategory) -> usize {
+        use WeakPointCategory::*;
+        match c {
+            UncheckedAllocation => 0,
+            UnboundedAllocation => 1,
+            UnboundedLoop => 2,
+            BlockingIO => 3,
+            UnsafeCode => 4,
+            PanicPath => 5,
+            RaceCondition => 6,
+            DeadlockPotential => 7,
+            ResourceLeak => 8,
+            CommandInjection => 9,
+            UnsafeDeserialization => 10,
+            DynamicCodeExecution => 11,
+            UnsafeFFI => 12,
+            AtomExhaustion => 13,
+            InsecureProtocol => 14,
+            ExcessivePermissions => 15,
+            PathTraversal => 16,
+            HardcodedSecret => 17,
+            UncheckedError => 18,
+            InfiniteRecursion => 19,
+            UnsafeTypeCoercion => 20,
+            ProofDrift => 21,
+            CryptoMisuse => 22,
+            SupplyChain => 23,
+            InputBoundary => 24,
+            MutationGap => 25,
+            LicensePolicy => 26,
+            Advisory => 27,
+            BannedDep => 28,
+            UnknownSource => 29,
+        }
+    }
+
+    #[test]
+    fn all_lists_every_variant_once_in_order() {
+        for (i, c) in WeakPointCategory::ALL.iter().enumerate() {
+            assert_eq!(ordinal(*c), i, "ALL[{i}] is {c:?}, out of place");
+        }
+    }
+
+    #[test]
+    fn rule_ids_are_unique() {
+        let ids: HashSet<&str> = WeakPointCategory::ALL.iter().map(|c| c.rule_id()).collect();
+        assert_eq!(
+            ids.len(),
+            WeakPointCategory::ALL.len(),
+            "two categories share a rule ID"
+        );
+    }
+
+    /// The published contract. Changing a line here renumbers a public
+    /// rule ID for every downstream consumer: do it only by owner decision.
+    #[test]
+    fn rule_ids_are_stable() {
+        let expected = [
+            "PA001", "PA001b", "PA002", "PA003", "PA004", "PA005", "PA006", "PA007", "PA008",
+            "PA009", "PA010", "PA011", "PA012", "PA013", "PA014", "PA015", "PA016", "PA017",
+            "PA018", "PA019", "PA020", "PA021", "PA022", "PA023", "PA024", "PA025", "PA026",
+            "PA027", "PA028", "PA029",
+        ];
+        let actual: Vec<&str> = WeakPointCategory::ALL.iter().map(|c| c.rule_id()).collect();
+        assert_eq!(actual, expected);
+    }
+}
@@ -6,7 +6,7 @@
 //! folds a *real* prover artifact end to end. This exercises that path against
 //! `tests/fixtures/proofs/UnsafeCodeSoundness.idr` — a genuine, `idris2
 //! --check`-clean, `%default total` Idris2 proof (no escape hatches) of the
-//! UnsafeCode (PA001) detector's soundness, carrying the `@name` / `@covers`
+//! UnsafeCode (PA004) detector's soundness, carrying the `@name` / `@covers`
 //! annotations the folder reads. It asserts the artifact is recognised as
 //! Idris2, classified `Closed` (no holes), hashed, named, and that the
 //! `sound:category:UnsafeCode` coverage is parsed.
 
@@ -3,7 +3,7 @@
 -- @name "UnsafeCode detector soundness (Idris2)"
 -- @covers sound:category:UnsafeCode
 |||
-||| A closed Idris2 soundness witness for panic-attack's UnsafeCode (PA001)
+||| A closed Idris2 soundness witness for panic-attack's UnsafeCode (PA004)
 ||| detector, in the exact shape `panic-attack aggregate` folds: no escape
 ||| hatches, a total proof that a positive detection is backed by a genuine
 ||| occurrence -- the detector raises no UnsafeCode finding on a token stream
 
@@ -2,7 +2,7 @@
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-//! Curated corpus for the UnboundedAllocation detector (PA015).
+//! Curated corpus for the UnboundedAllocation detector (PA001b).
 //!
 //! Each case is a minimal Rust source with a pre-declared expected
 //! verdict: does the detector correctly fire (or correctly not fire)