diff --git a/src/rust/corpus/acl2_books.rs b/src/rust/corpus/acl2_books.rs
index 79ee8014..632ab92d 100644
--- a/src/rust/corpus/acl2_books.rs
+++ b/src/rust/corpus/acl2_books.rs
@@ -320,9 +320,7 @@ fn classify_form(form: &str, line: usize, pf: &mut ParsedFile) {
     match head {
         "in-package" => {
             // (in-package "X")
-            let pkg = raw_arg1
-                .trim_matches('"')
-                .to_string();
+            let pkg = raw_arg1.trim_matches('"').to_string();
             if !pkg.is_empty() && pf.module_name.is_none() {
                 pf.module_name = Some(pkg);
             }
@@ -446,11 +444,9 @@ fn normalise_ws(s: &str) -> String {
 
 /// Tokenise on whitespace and Lisp syntactic glue.
 fn tokenise_idents(s: &str) -> Vec<&str> {
-    s.split(|c: char| {
-        c.is_whitespace() || matches!(c, '(' | ')' | '\'' | '`' | ',' | '"')
-    })
-    .filter(|t| !t.is_empty())
-    .collect()
+    s.split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '\'' | '`' | ',' | '"'))
+        .filter(|t| !t.is_empty())
+        .collect()
 }
 
 fn flag_hazards(text: &str, hz: &mut AxiomUsage) {
@@ -565,11 +561,12 @@ mod tests {
 ";
         let pf = parse_acl2_file(src);
         assert!(pf.imports.iter().any(|i| i == "std/lists/top"));
-        assert!(pf
-            .imports
+        assert!(pf.imports.iter().any(|i| i == "arithmetic/top-with-meta"));
+        let one = pf
+            .decls
             .iter()
-            .any(|i| i == "arithmetic/top-with-meta"));
-        let one = pf.decls.iter().find(|d| d.name == "*one*").expect("defconst");
+            .find(|d| d.name == "*one*")
+            .expect("defconst");
         assert_eq!(one.kind, DeclKind::Module);
     }
 }
diff --git a/src/rust/corpus/dafny.rs b/src/rust/corpus/dafny.rs
index 2adcdcae..80de4953 100644
--- a/src/rust/corpus/dafny.rs
+++ b/src/rust/corpus/dafny.rs
@@ -340,9 +340,7 @@ fn parse_dafny_file(raw: &str) -> ParsedFile {
             if let Some(after) = rest.strip_prefix(&prefix) {
                 let name = after
                     .chars()
-                    .take_while(|c| {
-                        c.is_alphanumeric() || *c == '_' || *c == '\'' || *c == '?'
-                    })
+                    .take_while(|c| c.is_alphanumeric() || *c == '_' || *c == '\'' || *c == '?')
                     .collect::<String>();
                 if name.is_empty() {
                     continue;
@@ -577,7 +575,8 @@ mod tests {
 
     #[test]
     fn detects_assume_hazard() {
-        let src = "module M {\n  lemma Sketchy()\n    ensures false\n  {\n    assume false;\n  }\n}\n";
+        let src =
+            "module M {\n  lemma Sketchy()\n    ensures false\n  {\n    assume false;\n  }\n}\n";
         let pf = parse_dafny_file(src);
         assert_eq!(pf.decls.len(), 1);
         assert_eq!(pf.decls[0].name, "Sketchy");
@@ -586,11 +585,7 @@ mod tests {
             "assume should set postulate hazard: {:?}",
             pf.decls[0].axiom_usage
         );
-        assert!(pf.decls[0]
-            .axiom_usage
-            .other
-            .iter()
-            .any(|s| s == "assume"));
+        assert!(pf.decls[0].axiom_usage.other.iter().any(|s| s == "assume"));
     }
 
     // Known heuristic-adapter limitation 2026-06-01: body-less `extern method`
diff --git a/src/rust/corpus/fstar.rs b/src/rust/corpus/fstar.rs
index f7f0fb6f..9ce767b6 100644
--- a/src/rust/corpus/fstar.rs
+++ b/src/rust/corpus/fstar.rs
@@ -545,12 +545,18 @@ type color =\n\
         let names: Vec<(&str, DeclKind)> =
             pf.decls.iter().map(|d| (d.name.as_str(), d.kind)).collect();
         assert!(
-            names.iter().any(|(n, k)| *n == "foo" && *k == DeclKind::Function),
-            "expected foo function, got {:?}", names
+            names
+                .iter()
+                .any(|(n, k)| *n == "foo" && *k == DeclKind::Function),
+            "expected foo function, got {:?}",
+            names
         );
         assert!(
-            names.iter().any(|(n, k)| *n == "color" && *k == DeclKind::Data),
-            "expected color data, got {:?}", names
+            names
+                .iter()
+                .any(|(n, k)| *n == "color" && *k == DeclKind::Data),
+            "expected color data, got {:?}",
+            names
         );
     }
 
@@ -566,11 +572,19 @@ assume Ax_no_lt : forall x. x >= 0\n\
 let cheat (x: nat) : nat = admit ()\n\
 ";
         let pf = parse_fstar_file(src);
-        let sketchy = pf.decls.iter().find(|d| d.name == "sketchy").expect("sketchy");
+        let sketchy = pf
+            .decls
+            .iter()
+            .find(|d| d.name == "sketchy")
+            .expect("sketchy");
         assert_eq!(sketchy.kind, DeclKind::Postulate);
         assert!(sketchy.axiom_usage.postulate);
 
-        let ax = pf.decls.iter().find(|d| d.name == "Ax_no_lt").expect("Ax_no_lt");
+        let ax = pf
+            .decls
+            .iter()
+            .find(|d| d.name == "Ax_no_lt")
+            .expect("Ax_no_lt");
         assert_eq!(ax.kind, DeclKind::Postulate);
         assert!(ax.axiom_usage.postulate);
 
diff --git a/src/rust/corpus/hol_light.rs b/src/rust/corpus/hol_light.rs
index e0e8c19d..b0c19d80 100644
--- a/src/rust/corpus/hol_light.rs
+++ b/src/rust/corpus/hol_light.rs
@@ -459,7 +459,10 @@ mod tests {
         assert_eq!(d.kind, DeclKind::Function);
         assert!(d.statement.contains("m + n"));
         let proof = d.proof.as_deref().unwrap_or("");
-        assert!(proof.contains("MESON_TAC"), "proof missing tactics: {proof}");
+        assert!(
+            proof.contains("MESON_TAC"),
+            "proof missing tactics: {proof}"
+        );
     }
 
     #[test]
diff --git a/src/rust/corpus/isabelle.rs b/src/rust/corpus/isabelle.rs
index 50b43507..c5fc9ef7 100644
--- a/src/rust/corpus/isabelle.rs
+++ b/src/rust/corpus/isabelle.rs
@@ -307,8 +307,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
 
         match kw {
             Some(k) if is_theorem_like(k) => {
-                let (consumed, decl) =
-                    parse_theorem_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_theorem_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -316,8 +315,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 continue;
             },
             Some(k) if is_definition_like(k) => {
-                let (consumed, decl) =
-                    parse_definition_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_definition_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -325,8 +323,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 continue;
             },
             Some(k) if is_data_like(k) => {
-                let (consumed, decl) =
-                    parse_data_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_data_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -334,8 +331,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 continue;
             },
             Some("record") => {
-                let (consumed, decl) =
-                    parse_data_like(&lines, &raw_lines, i, line_no, "record");
+                let (consumed, decl) = parse_data_like(&lines, &raw_lines, i, line_no, "record");
                 if let Some(mut d) = decl {
                     d.kind = DeclKind::Record;
                     pf.decls.push(d);
@@ -344,8 +340,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 continue;
             },
             Some(k @ ("axiomatization" | "axiom" | "consts")) => {
-                let (consumed, decl) =
-                    parse_postulate_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_postulate_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -357,8 +352,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 // Module-like DeclKind for sub-entries (Module is
                 // reserved for the file-level entry), so map to
                 // Function. Document keyword in the statement.
-                let (consumed, decl) =
-                    parse_definition_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_definition_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -477,8 +471,8 @@ fn parse_theorem_like(
     kw: &str,
 ) -> (usize, Option<DraftDecl>) {
     let first = lines[start].trim_start();
-    let name = extract_decl_name(first, kw)
-        .unwrap_or_else(|| format!("<anonymous-{}-L{}>", kw, line_no));
+    let name =
+        extract_decl_name(first, kw).unwrap_or_else(|| format!("<anonymous-{}-L{}>", kw, line_no));
 
     // Statement: accumulate lines until we see a proof opener
     // (`proof`, `by`, `apply`, `using`, `unfolding`, `including`,
diff --git a/src/rust/corpus/metamath.rs b/src/rust/corpus/metamath.rs
index e78912e2..7f199fcb 100644
--- a/src/rust/corpus/metamath.rs
+++ b/src/rust/corpus/metamath.rs
@@ -232,9 +232,7 @@ fn lex(src: &str) -> Vec<Token> {
         let is_ws = matches!(c, b' ' | b'\t' | b'\r' | b'\n');
         if is_ws {
             if let Some(s) = tok_start.take() {
-                let text = std::str::from_utf8(&bytes[s..i])
-                    .unwrap_or("")
-                    .to_string();
+                let text = std::str::from_utf8(&bytes[s..i]).unwrap_or("").to_string();
                 if !text.is_empty() {
                     out.push(Token {
                         text,
@@ -381,15 +379,18 @@ fn parse_mm_file(raw: &str) -> ParsedFile {
             }
             match kw {
                 "$c" | "$v" => {
-                    pf.options.push(format!("{}@{} {}", kw, line, payload.join(" ")));
+                    pf.options
+                        .push(format!("{}@{} {}", kw, line, payload.join(" ")));
                 },
                 "$d" => {
-                    pf.options.push(format!("$d@{} {}", line, payload.join(" ")));
+                    pf.options
+                        .push(format!("$d@{} {}", line, payload.join(" ")));
                 },
                 _ => {
                     // labelled forms reached without a preceding label
                     // (malformed); record as option for visibility.
-                    pf.options.push(format!("{}@{} (no label) {}", kw, line, payload.join(" ")));
+                    pf.options
+                        .push(format!("{}@{} (no label) {}", kw, line, payload.join(" ")));
                 },
             }
             i = j;
@@ -509,7 +510,10 @@ mod tests {
 
         let ax = pf.decls.iter().find(|d| d.name == "ax-mp").unwrap();
         assert_eq!(ax.kind, DeclKind::Postulate);
-        assert!(ax.axiom_usage.postulate, "ax-mp should be flagged as postulate");
+        assert!(
+            ax.axiom_usage.postulate,
+            "ax-mp should be flagged as postulate"
+        );
 
         let id = pf.decls.iter().find(|d| d.name == "id").unwrap();
         assert_eq!(id.kind, DeclKind::Function);
@@ -540,12 +544,7 @@ mod tests {
 
     #[test]
     fn scope_block_qualifies_label() {
-        let src = concat!(
-            "$c wff $.\n",
-            "${\n",
-            "inner $a wff bar $.\n",
-            "$}\n",
-        );
+        let src = concat!("$c wff $.\n", "${\n", "inner $a wff bar $.\n", "$}\n",);
         let pf = parse_mm_file(src);
         let inner = pf.decls.iter().find(|d| d.name == "inner").unwrap();
         assert!(
diff --git a/src/rust/corpus/minif2f.rs b/src/rust/corpus/minif2f.rs
index 8672e34b..db440c39 100644
--- a/src/rust/corpus/minif2f.rs
+++ b/src/rust/corpus/minif2f.rs
@@ -149,7 +149,7 @@ fn opening_tokens(ext: &str) -> &'static [&'static str] {
 /// Terminator tokens that end a proof body.
 fn terminators(ext: &str) -> &'static [&'static str] {
     match ext {
-        "lean" => &[],            // blank-line terminated; no `qed`
+        "lean" => &[], // blank-line terminated; no `qed`
         "thy" => &["qed", "done", "."],
         "ml" => &[";;"],
         "mm" => &["$."],
@@ -170,7 +170,12 @@ fn match_opening<'a>(line: &'a str, ext: &str) -> Option<(usize, String)> {
             let name: String = rest
                 .chars()
                 .take_while(|c| {
-                    !c.is_whitespace() && *c != '(' && *c != ':' && *c != '{' && *c != '[' && *c != ','
+                    !c.is_whitespace()
+                        && *c != '('
+                        && *c != ':'
+                        && *c != '{'
+                        && *c != '['
+                        && *c != ','
                 })
                 .collect();
             if !name.is_empty() {
@@ -306,7 +311,8 @@ mod tests {
 
     #[test]
     fn parses_lean_mathd_theorem() {
-        let src = "theorem mathd_algebra_42 (x : \u{211d}) (h : x + 1 = 2) : x = 1 := by\n  linarith\n";
+        let src =
+            "theorem mathd_algebra_42 (x : \u{211d}) (h : x + 1 = 2) : x = 1 := by\n  linarith\n";
         let decls = parse_uniform(src, "lean");
         assert_eq!(decls.len(), 1);
         assert_eq!(decls[0].name, "mathd_algebra_42");
@@ -343,11 +349,7 @@ mod tests {
         let decls = parse_uniform(src, "v");
         assert_eq!(decls.len(), 1);
         assert_eq!(decls[0].name, "amc_1985_p10");
-        assert!(decls[0]
-            .proof
-            .as_deref()
-            .unwrap()
-            .contains("reflexivity"));
+        assert!(decls[0].proof.as_deref().unwrap().contains("reflexivity"));
     }
 
     #[test]
@@ -355,10 +357,6 @@ mod tests {
         let src = "theorem mathd_empty : True\n";
         let decls = parse_uniform(src, "lean");
         assert_eq!(decls.len(), 1);
-        assert!(decls[0]
-            .axiom_usage
-            .other
-            .iter()
-            .any(|t| t == "empty_body"));
+        assert!(decls[0].axiom_usage.other.iter().any(|t| t == "empty_body"));
     }
 }
diff --git a/src/rust/corpus/mizar.rs b/src/rust/corpus/mizar.rs
index 59db3124..ffde21a3 100644
--- a/src/rust/corpus/mizar.rs
+++ b/src/rust/corpus/mizar.rs
@@ -240,18 +240,18 @@ fn parse_mizar_file(raw: &str) -> ParsedFile {
             head_keyword.as_deref(),
             Some(
                 "theorem"
-                | "definition"
-                | "scheme"
-                | "cluster"
-                | "registration"
-                | "notation"
-                | "synonym"
-                | "antonym"
-                | "attr"
-                | "mode"
-                | "func"
-                | "pred"
-                | "redefine"
+                    | "definition"
+                    | "scheme"
+                    | "cluster"
+                    | "registration"
+                    | "notation"
+                    | "synonym"
+                    | "antonym"
+                    | "attr"
+                    | "mode"
+                    | "func"
+                    | "pred"
+                    | "redefine"
             )
         );
 
@@ -376,8 +376,7 @@ fn find_keyword_at_word(s: &str, kw: &str) -> Option<usize> {
     while i + kwb.len() <= bytes.len() {
         if &bytes[i..i + kwb.len()] == kwb {
             let before_ok = i == 0 || !is_ident_byte(bytes[i - 1]);
-            let after_ok =
-                i + kwb.len() == bytes.len() || !is_ident_byte(bytes[i + kwb.len()]);
+            let after_ok = i + kwb.len() == bytes.len() || !is_ident_byte(bytes[i + kwb.len()]);
             if before_ok && after_ok {
                 return Some(i);
             }
@@ -425,9 +424,7 @@ fn collect_imports(env_text: &str, imports: &mut Vec<String>) {
 }
 
 fn is_plausible_article_id(s: &str) -> bool {
-    !s.is_empty()
-        && s.chars()
-            .all(|c| c.is_ascii_alphanumeric() || c == '_')
+    !s.is_empty() && s.chars().all(|c| c.is_ascii_alphanumeric() || c == '_')
 }
 
 /// Leading keyword (alphanumeric `_` run) at start of `s`.
@@ -453,8 +450,8 @@ fn classify_decl(kw: &str, head_line: &str) -> (String, DeclKind) {
     let (name, kind) = match kw {
         "theorem" => {
             // `theorem Th1: ...` (named) or `theorem ...` (unnamed).
-            let nm = parse_label_name(after_kw)
-                .unwrap_or_else(|| synthetic_name("Theorem", head_line));
+            let nm =
+                parse_label_name(after_kw).unwrap_or_else(|| synthetic_name("Theorem", head_line));
             (nm, DeclKind::Function)
         },
         "definition" => {
@@ -467,8 +464,8 @@ fn classify_decl(kw: &str, head_line: &str) -> (String, DeclKind) {
         },
         "scheme" => {
             // `scheme SchemeName { … } : … provided …`
-            let nm = parse_first_ident(after_kw)
-                .unwrap_or_else(|| synthetic_name("Scheme", head_line));
+            let nm =
+                parse_first_ident(after_kw).unwrap_or_else(|| synthetic_name("Scheme", head_line));
             (nm, DeclKind::Record)
         },
         "cluster" | "registration" => {
@@ -484,13 +481,11 @@ fn classify_decl(kw: &str, head_line: &str) -> (String, DeclKind) {
             (nm, DeclKind::Function)
         },
         "synonym" | "antonym" => {
-            let nm = parse_first_ident(after_kw)
-                .unwrap_or_else(|| synthetic_name(kw, head_line));
+            let nm = parse_first_ident(after_kw).unwrap_or_else(|| synthetic_name(kw, head_line));
             (nm, DeclKind::Function)
         },
         "attr" | "mode" | "func" | "pred" => {
-            let nm = parse_first_ident(after_kw)
-                .unwrap_or_else(|| synthetic_name(kw, head_line));
+            let nm = parse_first_ident(after_kw).unwrap_or_else(|| synthetic_name(kw, head_line));
             (nm, DeclKind::Function)
         },
         "redefine" => {
@@ -583,16 +578,7 @@ fn tokenise_idents(s: &str) -> Vec<&str> {
         c.is_whitespace()
             || matches!(
                 c,
-                '(' | ')'
-                    | '['
-                    | ']'
-                    | '{'
-                    | '}'
-                    | ','
-                    | ';'
-                    | ':'
-                    | '='
-                    | '.'
+                '(' | ')' | '[' | ']' | '{' | '}' | ',' | ';' | ':' | '=' | '.'
             )
     })
     .filter(|t| !t.is_empty())
@@ -647,7 +633,11 @@ mod tests {
         assert_eq!(pf.decls[0].kind, DeclKind::Function);
         assert!(pf.decls[0].statement.contains("for P being set"));
         let body = pf.decls[0].proof.as_deref().unwrap_or("");
-        assert!(body.contains("let P"), "proof body missing 'let P': {}", body);
+        assert!(
+            body.contains("let P"),
+            "proof body missing 'let P': {}",
+            body
+        );
         assert!(body.contains("thus P = P"));
         assert!(!pf.decls[0].axiom_usage.any());
     }
@@ -659,12 +649,12 @@ mod tests {
         assert_eq!(pf.decls.len(), 1);
         // `@proof` should set the sorry flag and append "@proof" to
         // the `other` hazard list.
-        assert!(pf.decls[0].axiom_usage.sorry, "sorry flag not set: {:?}", pf.decls[0].axiom_usage);
-        assert!(pf.decls[0]
-            .axiom_usage
-            .other
-            .iter()
-            .any(|s| s == "@proof"));
+        assert!(
+            pf.decls[0].axiom_usage.sorry,
+            "sorry flag not set: {:?}",
+            pf.decls[0].axiom_usage
+        );
+        assert!(pf.decls[0].axiom_usage.other.iter().any(|s| s == "@proof"));
     }
 
     #[test]
diff --git a/src/rust/corpus/mod.rs b/src/rust/corpus/mod.rs
index 5bd3681d..9fc0d91c 100644
--- a/src/rust/corpus/mod.rs
+++ b/src/rust/corpus/mod.rs
@@ -288,14 +288,20 @@ impl Corpus {
         let registry = MarkerRegistry::canonical();
         let adapter = self.adapter.clone();
         for entry in &mut self.entries {
-            entry.axiom_usage.other.retain(|s| !s.starts_with("discipline:"));
+            entry
+                .axiom_usage
+                .other
+                .retain(|s| !s.starts_with("discipline:"));
             let ctx = DetectionContext {
                 adapter: &adapter,
                 statement: &entry.statement,
                 proof: entry.proof.as_deref(),
             };
             for d in detect_disciplines(&ctx, &registry) {
-                entry.axiom_usage.other.push(format!("discipline:{}", d.tag()));
+                entry
+                    .axiom_usage
+                    .other
+                    .push(format!("discipline:{}", d.tag()));
             }
         }
     }
diff --git a/src/rust/corpus/smtlib.rs b/src/rust/corpus/smtlib.rs
index fe02cce8..bc0a8bf9 100644
--- a/src/rust/corpus/smtlib.rs
+++ b/src/rust/corpus/smtlib.rs
@@ -646,11 +646,7 @@ mod tests {
         .unwrap();
         let c = ingest(dir.path()).unwrap();
         let f = c.entries.iter().find(|e| e.name == "f").unwrap();
-        assert!(f
-            .axiom_usage
-            .other
-            .iter()
-            .any(|s| s == "uninterpreted"));
+        assert!(f.axiom_usage.other.iter().any(|s| s == "uninterpreted"));
     }
 
     #[test]
diff --git a/src/rust/corpus/tptp.rs b/src/rust/corpus/tptp.rs
index 0a19c5c4..73e10ff6 100644
--- a/src/rust/corpus/tptp.rs
+++ b/src/rust/corpus/tptp.rs
@@ -344,7 +344,9 @@ fn parse_tptp_file(raw: &str) -> ParsedFile {
                 // include arguments don't nest).
                 if let Some(end) = args.rfind(')') {
                     let inside = args[..end].trim();
-                    let path = inside.trim_matches(|c: char| c == '\'' || c == '"').to_string();
+                    let path = inside
+                        .trim_matches(|c: char| c == '\'' || c == '"')
+                        .to_string();
                     if !path.is_empty() && !pf.imports.contains(&path) {
                         pf.imports.push(path);
                     }
diff --git a/src/rust/disciplines/detector.rs b/src/rust/disciplines/detector.rs
index 4fde5169..d15e1d49 100644
--- a/src/rust/disciplines/detector.rs
+++ b/src/rust/disciplines/detector.rs
@@ -68,10 +68,7 @@ pub fn detect_disciplines(
         .into_iter()
         .filter(|(_, s)| *s >= DETECTION_THRESHOLD)
         .collect();
-    hits.sort_by(|a, b| {
-        b.1.partial_cmp(&a.1)
-            .unwrap_or(std::cmp::Ordering::Equal)
-    });
+    hits.sort_by(|a, b| b.1.partial_cmp(&a.1).unwrap_or(std::cmp::Ordering::Equal));
     hits.into_iter().map(|(d, _)| d).collect()
 }
 
diff --git a/src/rust/disciplines/mod.rs b/src/rust/disciplines/mod.rs
index 0059a10e..5e1febc5 100644
--- a/src/rust/disciplines/mod.rs
+++ b/src/rust/disciplines/mod.rs
@@ -60,11 +60,11 @@
 
 #![allow(dead_code)]
 
-pub mod registry;
 pub mod detector;
+pub mod registry;
 
-pub use registry::{DisciplineMarker, MarkerRegistry};
 pub use detector::{detect_disciplines, DetectionContext};
+pub use registry::{DisciplineMarker, MarkerRegistry};
 
 use serde::{Deserialize, Serialize};
 
diff --git a/src/rust/exchange/lambdapi.rs b/src/rust/exchange/lambdapi.rs
index 962b76d7..2f59209a 100644
--- a/src/rust/exchange/lambdapi.rs
+++ b/src/rust/exchange/lambdapi.rs
@@ -138,10 +138,8 @@ impl LambdapiExchange {
                 let rule = parse_rule(rest)?;
                 module.rules.push(rule);
             } else if stmt.starts_with("symbol ")
-                || SymbolKind::parse_modifier(
-                    stmt.split_whitespace().next().unwrap_or(""),
-                )
-                .is_some()
+                || SymbolKind::parse_modifier(stmt.split_whitespace().next().unwrap_or(""))
+                    .is_some()
             {
                 let sym = parse_symbol(stmt)?;
                 module.symbols.push(sym);
@@ -343,7 +341,10 @@ fn parse_symbol(stmt: &str) -> Result<LambdapiSymbol, ExchangeError> {
     }
     // rest now starts with: name : T [≔ body]
     let (name, after_name) = match rest.find(':') {
-        Some(i) => (rest[..i].trim().to_string(), rest[i + 1..].trim().to_string()),
+        Some(i) => (
+            rest[..i].trim().to_string(),
+            rest[i + 1..].trim().to_string(),
+        ),
         None => {
             return Err(ExchangeError::ParseError(format!(
                 "symbol missing ':' — {}",
diff --git a/src/rust/exchange/mod.rs b/src/rust/exchange/mod.rs
index 46cdf8f5..0711e1b1 100644
--- a/src/rust/exchange/mod.rs
+++ b/src/rust/exchange/mod.rs
@@ -19,11 +19,11 @@
 //! `docs/decisions/2026-06-01-saturation-campaign.md`.
 
 pub mod dedukti;
+pub mod lambdapi;
 pub mod opentheory;
-pub mod tptp;
-pub mod smtlib;
 pub mod smtcoq;
-pub mod lambdapi;
+pub mod smtlib;
+pub mod tptp;
 
 pub use dedukti::DeduktiExporter;
 pub use opentheory::OpenTheoryExporter;
diff --git a/src/rust/exchange/smtlib.rs b/src/rust/exchange/smtlib.rs
index 0cfd35aa..ce5418d7 100644
--- a/src/rust/exchange/smtlib.rs
+++ b/src/rust/exchange/smtlib.rs
@@ -41,10 +41,23 @@ impl std::error::Error for ExchangeError {}
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub enum SmtLibCommand {
     SetLogic(String),
-    SetInfo { key: String, value: String },
-    SetOption { key: String, value: String },
-    DeclareSort { name: String, arity: u32 },
-    DeclareFun { name: String, params: Vec<String>, ret: String },
+    SetInfo {
+        key: String,
+        value: String,
+    },
+    SetOption {
+        key: String,
+        value: String,
+    },
+    DeclareSort {
+        name: String,
+        arity: u32,
+    },
+    DeclareFun {
+        name: String,
+        params: Vec<String>,
+        ret: String,
+    },
     DefineFun {
         name: String,
         params: Vec<(String, String)>,
@@ -171,7 +184,11 @@ impl SmtLibExchange {
                 let body = body.trim();
                 let is_neg_conjecture = body.starts_with("(not ");
                 let formula = smt_expr_to_fof(body);
-                let role = if is_neg_conjecture { "conjecture" } else { "axiom" };
+                let role = if is_neg_conjecture {
+                    "conjecture"
+                } else {
+                    "axiom"
+                };
                 let name = format!("smt_{}", counter);
                 axioms.push(format!("fof({}, {}, {}).", name, role, formula));
                 counter += 1;
@@ -417,14 +434,12 @@ fn emit_command(cmd: &SmtLibCommand, out: &mut String) {
         SmtLibCommand::DeclareSort { name, arity } => {
             out.push_str(&format!("(declare-sort {} {})", name, arity))
         },
-        SmtLibCommand::DeclareFun { name, params, ret } => {
-            out.push_str(&format!(
-                "(declare-fun {} ({}) {})",
-                name,
-                params.join(" "),
-                ret
-            ))
-        },
+        SmtLibCommand::DeclareFun { name, params, ret } => out.push_str(&format!(
+            "(declare-fun {} ({}) {})",
+            name,
+            params.join(" "),
+            ret
+        )),
         SmtLibCommand::DefineFun {
             name,
             params,
diff --git a/src/rust/exchange/tptp.rs b/src/rust/exchange/tptp.rs
index b35742b7..8211fc13 100644
--- a/src/rust/exchange/tptp.rs
+++ b/src/rust/exchange/tptp.rs
@@ -147,7 +147,9 @@ pub struct TptpExchange {
 
 impl TptpExchange {
     pub fn new() -> Self {
-        Self { emit_comments: true }
+        Self {
+            emit_comments: true,
+        }
     }
 
     /// Import a TPTP source file into a structured problem.
@@ -280,10 +282,7 @@ impl TptpExchange {
         match problem.dialect {
             TptpDialect::Cnf | TptpDialect::Fof => {},
             d => {
-                return Err(ExchangeError::UnsupportedDialect(format!(
-                    "{:?}",
-                    d
-                )));
+                return Err(ExchangeError::UnsupportedDialect(format!("{:?}", d)));
             },
         }
         if problem.axioms.is_empty() && problem.conjecture.is_none() {
@@ -293,11 +292,7 @@ impl TptpExchange {
         out.push_str("(set-logic UF)\n");
         // Collect predicate / function symbols by a cheap lexical scan.
         let mut symbols: Vec<String> = Vec::new();
-        for f in problem
-            .axioms
-            .iter()
-            .chain(problem.conjecture.iter())
-        {
+        for f in problem.axioms.iter().chain(problem.conjecture.iter()) {
             collect_symbols(&f.formula, &mut symbols);
         }
         symbols.sort();
@@ -440,10 +435,7 @@ fn collect_symbols(formula: &str, into: &mut Vec<String>) {
         } else {
             if !current.is_empty() {
                 let token = current.clone();
-                if token
-                    .chars()
-                    .next()
-                    .is_some_and(|c| c.is_ascii_lowercase())
+                if token.chars().next().is_some_and(|c| c.is_ascii_lowercase())
                     && !matches!(
                         token.as_str(),
                         "true" | "false" | "and" | "or" | "not" | "implies"
diff --git a/src/rust/suggest/synonyms.rs b/src/rust/suggest/synonyms.rs
index 21837587..07817cdd 100644
--- a/src/rust/suggest/synonyms.rs
+++ b/src/rust/suggest/synonyms.rs
@@ -188,8 +188,8 @@ fn load_underscore_dict(dir: &Path, filename: &str) -> Result<SynonymTable> {
         return Ok(SynonymTable::default());
     }
     let raw = crate::provers::bounded_read_corpus_file(&path)?;
-    let parsed: RawTable = toml::from_str(&raw)
-        .with_context(|| format!("Failed to parse {}", path.display()))?;
+    let parsed: RawTable =
+        toml::from_str(&raw).with_context(|| format!("Failed to parse {}", path.display()))?;
     Ok(SynonymTable::from_entries(parsed.synonyms))
 }
 
diff --git a/src/rust/verification/dempster_shafer.rs b/src/rust/verification/dempster_shafer.rs
index c03fd04a..1f6683c0 100644
--- a/src/rust/verification/dempster_shafer.rs
+++ b/src/rust/verification/dempster_shafer.rs
@@ -61,11 +61,17 @@ impl VerdictSet {
     }
 
     fn contains_proven(self) -> bool {
-        matches!(self, VerdictSet::Proven | VerdictSet::ProvenOrRefuted | VerdictSet::Unknown)
+        matches!(
+            self,
+            VerdictSet::Proven | VerdictSet::ProvenOrRefuted | VerdictSet::Unknown
+        )
     }
 
     fn contains_refuted(self) -> bool {
-        matches!(self, VerdictSet::Refuted | VerdictSet::ProvenOrRefuted | VerdictSet::Unknown)
+        matches!(
+            self,
+            VerdictSet::Refuted | VerdictSet::ProvenOrRefuted | VerdictSet::Unknown
+        )
     }
 }
 
diff --git a/src/rust/verification/mod.rs b/src/rust/verification/mod.rs
index 81642f95..393c4fe7 100644
--- a/src/rust/verification/mod.rs
+++ b/src/rust/verification/mod.rs
@@ -30,17 +30,17 @@
 //! mechanism" entry in `docs/wiki/Guides.md`.
 
 pub mod axiom_tracker;
+pub mod bayesian_arbiter;
 pub mod certificates;
 pub mod confidence;
+pub mod dempster_shafer;
 pub mod mutation;
 pub mod pareto;
+pub mod pareto_arbiter;
 pub mod portfolio;
 #[cfg(feature = "verisim")]
 pub mod proof;
 pub mod statistics;
-pub mod bayesian_arbiter;
-pub mod dempster_shafer;
-pub mod pareto_arbiter;
 
 pub use axiom_tracker::{AxiomPolicy, AxiomTracker, AxiomUsage, DangerLevel};
 pub use certificates::{CertificateFormat, CertificateVerifier, ProofCertificate};
diff --git a/src/rust/verification/pareto_arbiter.rs b/src/rust/verification/pareto_arbiter.rs
index 7a369135..21d253d1 100644
--- a/src/rust/verification/pareto_arbiter.rs
+++ b/src/rust/verification/pareto_arbiter.rs
@@ -127,9 +127,11 @@ impl ParetoArbiter {
             Tiebreak::MinLatency => frontier
                 .iter()
                 .min_by_key(|o| (o.latency_ms, o.axiom_cost))?,
-            Tiebreak::MaxConfidence => frontier
-                .iter()
-                .max_by(|a, b| a.confidence.partial_cmp(&b.confidence).unwrap_or(std::cmp::Ordering::Equal))?,
+            Tiebreak::MaxConfidence => frontier.iter().max_by(|a, b| {
+                a.confidence
+                    .partial_cmp(&b.confidence)
+                    .unwrap_or(std::cmp::Ordering::Equal)
+            })?,
             Tiebreak::MinCertificate => frontier
                 .iter()
                 .min_by_key(|o| (o.certificate_size_bytes, o.latency_ms))?,