From 08b4a784dd579b98e898c83cd44a33258afc7b4b Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 2 Oct 2026 13:44:31 +0100
Subject: [PATCH 1/4] fix(ci): make Rust Build + rust-ci able to go green, and
 unmask clippy/fmt

- e2e.yml: `toolchain: v1` is not a toolchain name (rustup: "invalid
  toolchain name: 'v1'"), so "Rust Build + Unit Tests" died before
  building. Use `stable` with clippy + rustfmt components.
- e2e.yml: drop `|| true` from the Clippy and Format steps; they could
  never fail.
- cargo fmt over attestation.rs / keys_cli.rs (rust-ci's first red step).
- Clear every `clippy --all-targets -D warnings` lint (each target's
  errors masked the next): rand 0.9 thread_rng -> rng, needless mut /
  borrow / parens, &PathBuf -> &Path, dead `root_path` field, dead store
  in the transactions bench.
- jk-keys imported `attestation` and `keys` via `mod`, compiling a second
  private copy of each: the lib's public API read as dead code there and
  10 unit tests ran twice. Import them from the lib crate instead. Unique
  test count is unchanged (107; was 117 listed with the 10 duplicates).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
---
 .github/workflows/e2e.yml                     |  7 ++--
 benches/januskey_benchmarks.rs                |  5 +--
 crates/januskey-cli/src/attestation.rs        | 10 ++---
 crates/januskey-cli/src/keys.rs               | 12 +++---
 crates/januskey-cli/src/keys_cli.rs           | 19 ++++-----
 crates/januskey-cli/src/lib.rs                |  6 +--
 crates/januskey-cli/src/main.rs               | 39 +++++++++----------
 crates/januskey-cli/src/obliteration.rs       |  8 ++--
 crates/januskey-cli/src/operations.rs         |  6 +--
 crates/januskey-cli/tests/aspect_test.rs      | 18 ++++-----
 crates/januskey-cli/tests/concurrency_test.rs | 19 ++++-----
 crates/januskey-cli/tests/e2e_test.rs         | 28 ++++++-------
 crates/januskey-cli/tests/p2p_test.rs         | 10 ++---
 crates/reversible-core/src/manifest.rs        |  4 +-
 crates/reversible-core/src/metadata.rs        |  2 +-
 crates/reversible-core/src/transaction.rs     |  2 +-
 16 files changed, 87 insertions(+), 108 deletions(-)

diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index 2acf914..3e23f5c 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -21,16 +21,17 @@ jobs:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
         with:
-          toolchain: v1
+          toolchain: stable
+          components: clippy, rustfmt
       - uses: Swatinem/rust-cache@v2.9.2
       - name: Build
         run: cargo build --release
       - name: Unit + P2P tests
         run: cargo test --all -- --test-threads=1
       - name: Clippy
-        run: cargo clippy --all -- -D warnings || true
+        run: cargo clippy --all --all-targets -- -D warnings
       - name: Format check
-        run: cargo fmt --all -- --check || true
+        run: cargo fmt --all -- --check
 
   benchmarks:
     name: Criterion Benchmarks
diff --git a/benches/januskey_benchmarks.rs b/benches/januskey_benchmarks.rs
index bee8f95..21ec34c 100644
--- a/benches/januskey_benchmarks.rs
+++ b/benches/januskey_benchmarks.rs
@@ -117,9 +117,8 @@ fn bench_transactions(c: &mut Criterion) {
 
     group.bench_function("begin_commit", |b| {
         b.iter(|| {
-            let mut active = false;
             // Begin
-            active = true;
+            let mut active = true;
             black_box(active);
             // Commit
             active = false;
@@ -156,7 +155,7 @@ fn bench_key_derivation(c: &mut Criterion) {
 
             for _ in 0..1000 {
                 let mut hasher = Sha256::new();
-                hasher.update(&hash);
+                hasher.update(hash);
                 hash.copy_from_slice(&hasher.finalize());
             }
             black_box(hash);
diff --git a/crates/januskey-cli/src/attestation.rs b/crates/januskey-cli/src/attestation.rs
index daf7e46..08e54d3 100644
--- a/crates/januskey-cli/src/attestation.rs
+++ b/crates/januskey-cli/src/attestation.rs
@@ -200,11 +200,7 @@ impl AuditLog {
     /// Errors if no attestation key is set: an unkeyed attestation is
     /// forgeable and must never be silently produced (the previous
     /// `unwrap_or([0u8; 32])` all-zero-key fallback did exactly that).
-    fn compute_attestation(
-        &self,
-        data: &str,
-        previous_hash: &str,
-    ) -> std::io::Result<String> {
+    fn compute_attestation(&self, data: &str, previous_hash: &str) -> std::io::Result<String> {
         let key = self.attestation_key.ok_or_else(|| {
             std::io::Error::new(
                 std::io::ErrorKind::PermissionDenied,
@@ -213,8 +209,8 @@ impl AuditLog {
             )
         })?;
 
-        let mut mac = <Hmac<Sha256>>::new_from_slice(&key)
-            .expect("HMAC accepts keys of any length");
+        let mut mac =
+            <Hmac<Sha256>>::new_from_slice(&key).expect("HMAC accepts keys of any length");
         mac.update(Self::ATTESTATION_SCHEME.as_bytes());
         mac.update(b"\x00");
         mac.update(data.as_bytes());
diff --git a/crates/januskey-cli/src/keys.rs b/crates/januskey-cli/src/keys.rs
index 19193dc..117f4a3 100644
--- a/crates/januskey-cli/src/keys.rs
+++ b/crates/januskey-cli/src/keys.rs
@@ -184,7 +184,7 @@ impl SecretKey {
 
     pub fn generate() -> Result<Self> {
         let mut bytes = [0u8; KEY_LENGTH];
-        rand::thread_rng().fill_bytes(&mut bytes);
+        rand::rng().fill_bytes(&mut bytes);
         Ok(Self { bytes })
     }
 }
@@ -192,7 +192,6 @@ impl SecretKey {
 /// Key manager for JanusKey
 pub struct KeyManager {
     store_path: PathBuf,
-    root_path: PathBuf,
     kek: Option<SecretKey>,
     audit_log: AuditLog,
 }
@@ -204,7 +203,6 @@ impl KeyManager {
         let audit_log = AuditLog::new(root);
         Self {
             store_path,
-            root_path: root.to_path_buf(),
             kek: None,
             audit_log,
         }
@@ -230,7 +228,7 @@ impl KeyManager {
 
         // Generate salt
         let mut salt = [0u8; SALT_LENGTH];
-        rand::thread_rng().fill_bytes(&mut salt);
+        rand::rng().fill_bytes(&mut salt);
 
         // Derive KEK from passphrase
         let kek = derive_kek(passphrase, &salt)?;
@@ -246,7 +244,7 @@ impl KeyManager {
 
         // Generate initial nonce
         let mut nonce = [0u8; NONCE_LENGTH];
-        rand::thread_rng().fill_bytes(&mut nonce);
+        rand::rng().fill_bytes(&mut nonce);
 
         // Create empty key store
         let store = KeyStoreData {
@@ -548,7 +546,7 @@ impl KeyManager {
         let path = self.store_path.join("keystore.jks");
         let content = ({
             use std::io::Read;
-            std::fs::File::open(&path).and_then(|mut f| {
+            std::fs::File::open(&path).and_then(|f| {
                 let mut buf = String::new();
                 f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                 Ok(buf)
@@ -607,7 +605,7 @@ fn derive_kek(passphrase: &str, salt: &[u8; SALT_LENGTH]) -> Result<SecretKey> {
 /// Wrap (encrypt) key material
 fn wrap_key(kek: &SecretKey, key: &[u8], metadata: &KeyMetadata) -> Result<WrappedKey> {
     let mut nonce_bytes = [0u8; NONCE_LENGTH];
-    rand::thread_rng().fill_bytes(&mut nonce_bytes);
+    rand::rng().fill_bytes(&mut nonce_bytes);
 
     let cipher = Aes256Gcm::new(kek.as_bytes().into());
     let nonce = Nonce::from_slice(&nonce_bytes);
diff --git a/crates/januskey-cli/src/keys_cli.rs b/crates/januskey-cli/src/keys_cli.rs
index a9197c6..cd7833e 100644
--- a/crates/januskey-cli/src/keys_cli.rs
+++ b/crates/januskey-cli/src/keys_cli.rs
@@ -8,12 +8,12 @@
 use clap::{Parser, Subcommand};
 use colored::Colorize;
 use dialoguer::{Confirm, Password};
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 use uuid::Uuid;
 
-mod attestation;
-mod keys;
 use attestation::AuditEventType;
+use januskey::attestation;
+use januskey::keys;
 use keys::{KeyAlgorithm, KeyManager, KeyPurpose, KeyState};
 
 #[derive(Parser)]
@@ -293,9 +293,7 @@ fn cmd_generate(
             )
             .into())
         }
-        _ => {
-            return Err(format!("Unknown key type: {}. Use: aes256", key_type).into())
-        }
+        _ => return Err(format!("Unknown key type: {}. Use: aes256", key_type).into()),
     };
 
     let key_purpose = match purpose.to_lowercase().as_str() {
@@ -447,7 +445,7 @@ fn cmd_revoke(
     Ok(())
 }
 
-fn cmd_backup(km: &mut KeyManager, output: &PathBuf) -> Result<(), Box<dyn std::error::Error>> {
+fn cmd_backup(km: &mut KeyManager, output: &Path) -> Result<(), Box<dyn std::error::Error>> {
     unlock_store(km)?;
 
     if output.exists() {
@@ -567,7 +565,7 @@ fn cmd_audit_show(km: &mut KeyManager, limit: usize) -> Result<(), Box<dyn std::
         };
 
         let details = if let Some(ref kd) = entry.key_details {
-            format!("key:{}", &kd.fingerprint)
+            format!("key:{}", kd.fingerprint)
         } else if let Some(ref reason) = entry.reason {
             if reason.len() > 30 {
                 format!("{}...", &reason[..27])
@@ -675,10 +673,7 @@ fn cmd_audit_verify(km: &mut KeyManager) -> Result<(), Box<dyn std::error::Error
     Ok(())
 }
 
-fn cmd_audit_export(
-    km: &mut KeyManager,
-    output: &PathBuf,
-) -> Result<(), Box<dyn std::error::Error>> {
+fn cmd_audit_export(km: &mut KeyManager, output: &Path) -> Result<(), Box<dyn std::error::Error>> {
     unlock_store(km)?;
 
     if output.exists() {
diff --git a/crates/januskey-cli/src/lib.rs b/crates/januskey-cli/src/lib.rs
index 6157bf7..f7d39c0 100644
--- a/crates/januskey-cli/src/lib.rs
+++ b/crates/januskey-cli/src/lib.rs
@@ -76,14 +76,14 @@ impl Config {
     pub fn load(dir: &std::path::Path) -> Self {
         let config_path = dir.join(".januskey").join("config.json");
         if config_path.exists() {
-            if let Ok(content) = ({
+            if let Ok(content) = {
                 use std::io::Read;
-                std::fs::File::open(&config_path).and_then(|mut f| {
+                std::fs::File::open(&config_path).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
                 })
-            }) {
+            } {
                 if let Ok(config) = serde_json::from_str(&content) {
                     return config;
                 }
diff --git a/crates/januskey-cli/src/main.rs b/crates/januskey-cli/src/main.rs
index 603392a..182bdc6 100644
--- a/crates/januskey-cli/src/main.rs
+++ b/crates/januskey-cli/src/main.rs
@@ -15,8 +15,7 @@ use januskey::{
     transaction::TransactionPreview,
     JanusKey,
 };
-use std::fs;
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 
 #[derive(Parser)]
 #[command(
@@ -217,7 +216,7 @@ fn main() -> Result<()> {
     }
 }
 
-fn cmd_init(dir: &PathBuf) -> Result<()> {
+fn cmd_init(dir: &Path) -> Result<()> {
     if JanusKey::is_initialized(dir) {
         println!(
             "{} JanusKey already initialized in {}",
@@ -239,7 +238,7 @@ fn cmd_init(dir: &PathBuf) -> Result<()> {
 }
 
 fn cmd_delete(
-    dir: &PathBuf,
+    dir: &Path,
     paths: &[String],
     recursive: bool,
     dry_run: bool,
@@ -360,7 +359,7 @@ fn cmd_delete(
 }
 
 fn cmd_modify(
-    dir: &PathBuf,
+    dir: &Path,
     pattern: &str,
     paths: &[String],
     dry_run: bool,
@@ -394,7 +393,7 @@ fn cmd_modify(
     for file in &files {
         let content = ({
             use std::io::Read;
-            std::fs::File::open(file).and_then(|mut f| {
+            std::fs::File::open(file).and_then(|f| {
                 let mut buf = String::new();
                 f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                 Ok(buf)
@@ -480,12 +479,12 @@ fn parse_sed_pattern(pattern: &str) -> Result<(String, String, bool)> {
 
     let search = parts[0].to_string();
     let replace = parts[1].to_string();
-    let global = parts.get(2).map_or(false, |f| f.contains('g'));
+    let global = parts.get(2).is_some_and(|f| f.contains('g'));
 
     Ok((search, replace, global))
 }
 
-fn cmd_move(dir: &PathBuf, source: &str, destination: &PathBuf, dry_run: bool) -> Result<()> {
+fn cmd_move(dir: &Path, source: &str, destination: &PathBuf, dry_run: bool) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let source_path = if PathBuf::from(source).is_absolute() {
@@ -536,7 +535,7 @@ fn cmd_move(dir: &PathBuf, source: &str, destination: &PathBuf, dry_run: bool) -
     Ok(())
 }
 
-fn cmd_copy(dir: &PathBuf, source: &PathBuf, destination: &PathBuf, dry_run: bool) -> Result<()> {
+fn cmd_copy(dir: &Path, source: &PathBuf, destination: &PathBuf, dry_run: bool) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let source_path = if source.is_absolute() {
@@ -592,7 +591,7 @@ fn cmd_copy(dir: &PathBuf, source: &PathBuf, destination: &PathBuf, dry_run: boo
 /// purge its operation-log entries (recording each shred in
 /// `.januskey/obliterations.json`); otherwise only the working files are
 /// shredded.
-fn cmd_obliterate(dir: &PathBuf, paths: &[PathBuf], dry_run: bool, auto_yes: bool) -> Result<()> {
+fn cmd_obliterate(dir: &Path, paths: &[PathBuf], dry_run: bool, auto_yes: bool) -> Result<()> {
     use januskey::obliteration::{
         obliterate_file, obliterate_path, ObliterationManager, OBLITERATION_LOG_FILE,
     };
@@ -713,7 +712,7 @@ fn cmd_obliterate(dir: &PathBuf, paths: &[PathBuf], dry_run: bool, auto_yes: boo
     Ok(())
 }
 
-fn cmd_undo(dir: &PathBuf, count: usize, id: Option<String>) -> Result<()> {
+fn cmd_undo(dir: &Path, count: usize, id: Option<String>) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     if let Some(op_id) = id {
@@ -767,7 +766,7 @@ fn cmd_undo(dir: &PathBuf, count: usize, id: Option<String>) -> Result<()> {
     Ok(())
 }
 
-fn cmd_begin(dir: &PathBuf, name: Option<String>) -> Result<()> {
+fn cmd_begin(dir: &Path, name: Option<String>) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let tx = jk.transaction_manager.begin(name.clone())?;
@@ -786,7 +785,7 @@ fn cmd_begin(dir: &PathBuf, name: Option<String>) -> Result<()> {
     Ok(())
 }
 
-fn cmd_commit(dir: &PathBuf) -> Result<()> {
+fn cmd_commit(dir: &Path) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let tx = jk.transaction_manager.commit()?;
@@ -801,7 +800,7 @@ fn cmd_commit(dir: &PathBuf) -> Result<()> {
     Ok(())
 }
 
-fn cmd_rollback(dir: &PathBuf) -> Result<()> {
+fn cmd_rollback(dir: &Path) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     // Get the active transaction's operation IDs before modifying state
@@ -830,7 +829,7 @@ fn cmd_rollback(dir: &PathBuf) -> Result<()> {
     Ok(())
 }
 
-fn cmd_preview(dir: &PathBuf) -> Result<()> {
+fn cmd_preview(dir: &Path) -> Result<()> {
     let jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let tx = jk
@@ -843,7 +842,7 @@ fn cmd_preview(dir: &PathBuf) -> Result<()> {
     let name = preview
         .transaction_name
         .unwrap_or_else(|| tx.id[..8].to_string());
-    println!("{} Transaction: {}", "📋".to_string(), name.cyan());
+    println!("📋 Transaction: {}", name.cyan());
     println!("Operations pending: {}", preview.operations.len());
     println!();
 
@@ -887,7 +886,7 @@ fn cmd_preview(dir: &PathBuf) -> Result<()> {
     Ok(())
 }
 
-fn cmd_history(dir: &PathBuf, limit: usize, filter: Option<String>) -> Result<()> {
+fn cmd_history(dir: &Path, limit: usize, filter: Option<String>) -> Result<()> {
     let jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let ops: Vec<_> = if let Some(ref filter_str) = filter {
@@ -949,7 +948,7 @@ fn cmd_history(dir: &PathBuf, limit: usize, filter: Option<String>) -> Result<()
     Ok(())
 }
 
-fn cmd_status(dir: &PathBuf) -> Result<()> {
+fn cmd_status(dir: &Path) -> Result<()> {
     let jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     println!("{}", "JanusKey Status".bold());
@@ -965,7 +964,7 @@ fn cmd_status(dir: &PathBuf) -> Result<()> {
     if let Some(tx) = jk.transaction_manager.active() {
         let name = tx.name.clone().unwrap_or_else(|| tx.id[..8].to_string());
         println!();
-        println!("{} Active transaction: {}", "📝".to_string(), name.cyan());
+        println!("📝 Active transaction: {}", name.cyan());
         println!("  Started: {}", tx.started_at.format("%Y-%m-%d %H:%M:%S"));
         println!("  Operations: {}", tx.operation_ids.len());
     } else {
@@ -976,7 +975,7 @@ fn cmd_status(dir: &PathBuf) -> Result<()> {
     Ok(())
 }
 
-fn cmd_gc(dir: &PathBuf, keep: Option<usize>, _older_than: Option<u32>) -> Result<()> {
+fn cmd_gc(dir: &Path, keep: Option<usize>, _older_than: Option<u32>) -> Result<()> {
     let mut jk = JanusKey::open(dir).context("Failed to open JanusKey directory")?;
 
     let keep_count = keep.unwrap_or(jk.config.max_history);
diff --git a/crates/januskey-cli/src/obliteration.rs b/crates/januskey-cli/src/obliteration.rs
index 546f0ba..c00f8fd 100644
--- a/crates/januskey-cli/src/obliteration.rs
+++ b/crates/januskey-cli/src/obliteration.rs
@@ -73,13 +73,13 @@ impl ObliterationProof {
 
         // Generate random nonce
         let mut nonce_bytes = [0u8; 32];
-        rand::thread_rng().fill_bytes(&mut nonce_bytes);
+        rand::rng().fill_bytes(&mut nonce_bytes);
         let nonce = hex::encode(nonce_bytes);
 
         // Generate commitment: H(content_hash || nonce || timestamp)
         let mut hasher = Sha256::new();
         hasher.update(content_hash.raw_hash().as_bytes());
-        hasher.update(&nonce_bytes);
+        hasher.update(nonce_bytes);
         hasher.update(timestamp.to_rfc3339().as_bytes());
         let commitment = hex::encode(hasher.finalize());
 
@@ -163,7 +163,7 @@ impl ObliterationManager {
         let log = if log_path.exists() {
             let content = ({
                 use std::io::Read;
-                std::fs::File::open(&log_path).and_then(|mut f| {
+                std::fs::File::open(&log_path).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
@@ -342,7 +342,7 @@ fn secure_overwrite(path: &Path) -> Result<usize> {
         let buffer = if pass == OVERWRITE_PASSES - 1 {
             // Final pass: random data
             let mut random_buffer = vec![0u8; file_size.min(8192)];
-            rand::thread_rng().fill_bytes(&mut random_buffer);
+            rand::rng().fill_bytes(&mut random_buffer);
             random_buffer
         } else {
             // Fixed pattern
diff --git a/crates/januskey-cli/src/operations.rs b/crates/januskey-cli/src/operations.rs
index 2813ca0..29803fe 100644
--- a/crates/januskey-cli/src/operations.rs
+++ b/crates/januskey-cli/src/operations.rs
@@ -500,7 +500,7 @@ mod tests {
         assert_eq!(
             ({
                 use std::io::Read;
-                std::fs::File::open(&test_file).and_then(|mut f| {
+                std::fs::File::open(&test_file).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
@@ -531,7 +531,7 @@ mod tests {
         assert_eq!(
             ({
                 use std::io::Read;
-                std::fs::File::open(&test_file).and_then(|mut f| {
+                std::fs::File::open(&test_file).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
@@ -548,7 +548,7 @@ mod tests {
         assert_eq!(
             ({
                 use std::io::Read;
-                std::fs::File::open(&test_file).and_then(|mut f| {
+                std::fs::File::open(&test_file).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
diff --git a/crates/januskey-cli/tests/aspect_test.rs b/crates/januskey-cli/tests/aspect_test.rs
index a9fc372..e4cfa1a 100644
--- a/crates/januskey-cli/tests/aspect_test.rs
+++ b/crates/januskey-cli/tests/aspect_test.rs
@@ -9,7 +9,7 @@
 //   - Overwrite patterns applied correctly (3-pass DoD 5220.22-M)
 
 use std::fs;
-use std::path::PathBuf;
+use std::path::Path;
 use tempfile::TempDir;
 
 /// Helper: Create temp directory
@@ -18,7 +18,7 @@ fn test_dir() -> TempDir {
 }
 
 /// Helper: Create jk directories
-fn setup_jk_dirs(base: &PathBuf) -> std::io::Result<()> {
+fn setup_jk_dirs(base: &Path) -> std::io::Result<()> {
     fs::create_dir_all(base.join(".jk/content"))?;
     fs::create_dir_all(base.join(".jk/obliteration"))?;
     fs::create_dir_all(base.join(".jk/keys"))?;
@@ -26,7 +26,7 @@ fn setup_jk_dirs(base: &PathBuf) -> std::io::Result<()> {
 }
 
 /// Helper: Create a test key file and record
-fn create_test_key(base: &PathBuf, key_id: &str, material: &[u8]) -> String {
+fn create_test_key(base: &Path, key_id: &str, material: &[u8]) -> String {
     use sha2::{Digest, Sha256};
 
     let mut hasher = Sha256::new();
@@ -143,13 +143,11 @@ fn obliterated_key_record_marked_revoked() {
     // Verify key record reflects revocation
     let key_content = ({
         use std::io::Read;
-        std::fs::File::open(base.join(".jk/keys").join(format!("{}.json", key_id))).and_then(
-            |mut f| {
-                let mut buf = String::new();
-                f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
-                Ok(buf)
-            },
-        )
+        std::fs::File::open(base.join(".jk/keys").join(format!("{}.json", key_id))).and_then(|f| {
+            let mut buf = String::new();
+            f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
+            Ok(buf)
+        })
     })
     .expect("Read key record");
     assert!(
diff --git a/crates/januskey-cli/tests/concurrency_test.rs b/crates/januskey-cli/tests/concurrency_test.rs
index 81ba781..e4226e7 100644
--- a/crates/januskey-cli/tests/concurrency_test.rs
+++ b/crates/januskey-cli/tests/concurrency_test.rs
@@ -9,7 +9,7 @@
 //   - Race conditions in commit/rollback don't corrupt state
 
 use std::fs;
-use std::path::PathBuf;
+use std::path::Path;
 use std::sync::{Arc, Mutex};
 use tempfile::TempDir;
 
@@ -19,7 +19,7 @@ fn test_dir() -> TempDir {
 }
 
 /// Helper: Setup jk directories
-fn setup_jk_dirs(base: &PathBuf) -> std::io::Result<()> {
+fn setup_jk_dirs(base: &Path) -> std::io::Result<()> {
     fs::create_dir_all(base.join(".jk/content"))?;
     fs::create_dir_all(base.join(".jk/transactions"))?;
     fs::create_dir_all(base.join(".jk/operations"))?;
@@ -60,7 +60,7 @@ fn concurrent_key_operations_no_deadlock() {
 
             // Write content
             fs::write(&content_path, material.as_bytes())
-                .expect(&format!("Write failed for {}", key_id));
+                .unwrap_or_else(|_| panic!("Write failed for {}", key_id));
 
             // Record key
             let key_record = format!(r#"{{"id":"{}","hash":"{}","thread":{}}}"#, key_id, hash, i);
@@ -68,10 +68,11 @@ fn concurrent_key_operations_no_deadlock() {
                 base_clone.join(".jk/keys").join(format!("{}.json", key_id)),
                 &key_record,
             )
-            .expect(&format!("Key record failed for {}", key_id));
+            .unwrap_or_else(|_| panic!("Key record failed for {}", key_id));
 
             // Read back immediately
-            let read_back = fs::read(&content_path).expect(&format!("Read failed for {}", key_id));
+            let read_back =
+                fs::read(&content_path).unwrap_or_else(|_| panic!("Read failed for {}", key_id));
             assert_eq!(
                 read_back,
                 material.as_bytes(),
@@ -127,12 +128,12 @@ fn transaction_isolation_uncommitted_invisible() {
 
         let ops_dir = base_clone.join(".jk/operations");
         let ops: Vec<_> = fs::read_dir(&ops_dir)
-            .unwrap_or_else(|_| fs::read_dir(&base_clone.join(".jk")).unwrap())
+            .unwrap_or_else(|_| fs::read_dir(base_clone.join(".jk")).unwrap())
             .filter_map(Result::ok)
             .filter(|e| {
                 e.file_name()
                     .to_str()
-                    .map_or(false, |n| n.contains(&tx_id_clone))
+                    .is_some_and(|n| n.contains(&tx_id_clone))
             })
             .collect();
 
@@ -159,7 +160,7 @@ fn transaction_isolation_uncommitted_invisible() {
     // but we verify the transaction itself is still "active" not "committed"
     let tx_read = ({
         use std::io::Read;
-        std::fs::File::open(base.join(".jk/transactions/001.json")).and_then(|mut f| {
+        std::fs::File::open(base.join(".jk/transactions/001.json")).and_then(|f| {
             let mut buf = String::new();
             f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
             Ok(buf)
@@ -388,7 +389,7 @@ fn concurrent_commit_rollback_no_corruption() {
         let entry = entry.expect("Dir entry");
         let content = ({
             use std::io::Read;
-            std::fs::File::open(entry.path()).and_then(|mut f| {
+            std::fs::File::open(entry.path()).and_then(|f| {
                 let mut buf = String::new();
                 f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                 Ok(buf)
diff --git a/crates/januskey-cli/tests/e2e_test.rs b/crates/januskey-cli/tests/e2e_test.rs
index 9641a49..4566755 100644
--- a/crates/januskey-cli/tests/e2e_test.rs
+++ b/crates/januskey-cli/tests/e2e_test.rs
@@ -7,7 +7,7 @@
 // Content roundtrip: write → hash → read → delete
 
 use std::fs;
-use std::path::PathBuf;
+use std::path::Path;
 use tempfile::TempDir;
 
 /// Helper: Create a temp directory for test isolation
@@ -16,7 +16,7 @@ fn test_dir() -> TempDir {
 }
 
 /// Helper: Create jk directories
-fn setup_jk_dirs(base: &PathBuf) -> std::io::Result<()> {
+fn setup_jk_dirs(base: &Path) -> std::io::Result<()> {
     fs::create_dir_all(base.join(".jk/content"))?;
     fs::create_dir_all(base.join(".jk/metadata"))?;
     fs::create_dir_all(base.join(".jk/attestation"))?;
@@ -85,7 +85,7 @@ fn full_key_lifecycle_single_key() {
     // Step 5: Verify attestation references the key
     let attest_read = ({
         use std::io::Read;
-        std::fs::File::open(base.join(".jk/attestation/0001.json")).and_then(|mut f| {
+        std::fs::File::open(base.join(".jk/attestation/0001.json")).and_then(|f| {
             let mut buf = String::new();
             f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
             Ok(buf)
@@ -104,7 +104,7 @@ fn full_key_lifecycle_single_key() {
     // Verify key record exists
     let key_read = ({
         use std::io::Read;
-        std::fs::File::open(base.join(".jk/keys/001.json")).and_then(|mut f| {
+        std::fs::File::open(base.join(".jk/keys/001.json")).and_then(|f| {
             let mut buf = String::new();
             f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
             Ok(buf)
@@ -134,7 +134,7 @@ fn full_key_lifecycle_multi_key_transaction() {
 
     for (i, (key_id, material)) in keys.iter().enumerate() {
         // Store content
-        let hash = sha256(*material);
+        let hash = sha256(material);
         let content_path = base.join(".jk/content").join(&hash);
         fs::write(&content_path, material).expect("Store content");
 
@@ -173,11 +173,7 @@ fn full_key_lifecycle_multi_key_transaction() {
     let op_files: Vec<_> = fs::read_dir(base.join(".jk/operations"))
         .expect("Read ops dir")
         .filter_map(Result::ok)
-        .filter(|e| {
-            e.file_name()
-                .to_str()
-                .map_or(false, |n| n.starts_with(tx_id))
-        })
+        .filter(|e| e.file_name().to_str().is_some_and(|n| n.starts_with(tx_id)))
         .collect();
     assert_eq!(op_files.len(), 3, "Transaction must contain 3 operations");
 
@@ -188,7 +184,7 @@ fn full_key_lifecycle_multi_key_transaction() {
     // Verify transaction is committed
     let tx_read = ({
         use std::io::Read;
-        std::fs::File::open(base.join(".jk/transactions/001.json")).and_then(|mut f| {
+        std::fs::File::open(base.join(".jk/transactions/001.json")).and_then(|f| {
             let mut buf = String::new();
             f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
             Ok(buf)
@@ -239,13 +235,13 @@ fn delta_chain_full_history() {
     fs::write(base.join(".jk/metadata/delta-02.json"), &delta_2_to_3).expect("Write delta 2→3");
 
     // Verify chain is intact: can read all versions
-    let read_v1 = fs::read(&base.join(".jk/content").join(&v1_hash)).expect("Read v1");
+    let read_v1 = fs::read(base.join(".jk/content").join(&v1_hash)).expect("Read v1");
     assert_eq!(read_v1, v1, "Version 1 must be recoverable");
 
-    let read_v2 = fs::read(&base.join(".jk/content").join(&v2_hash)).expect("Read v2");
+    let read_v2 = fs::read(base.join(".jk/content").join(&v2_hash)).expect("Read v2");
     assert_eq!(read_v2, v2, "Version 2 must be recoverable");
 
-    let read_v3 = fs::read(&base.join(".jk/content").join(&v3_hash)).expect("Read v3");
+    let read_v3 = fs::read(base.join(".jk/content").join(&v3_hash)).expect("Read v3");
     assert_eq!(read_v3, v3, "Version 3 must be recoverable");
 
     // Verify chain links are recorded
@@ -255,7 +251,7 @@ fn delta_chain_full_history() {
         .filter(|e| {
             e.file_name()
                 .to_str()
-                .map_or(false, |n| n.starts_with("delta"))
+                .is_some_and(|n| n.starts_with("delta"))
         })
         .collect();
     assert_eq!(delta_files.len(), 2, "Delta chain must have 2 links");
@@ -377,7 +373,7 @@ fn corrupted_attestation_entry_detected() {
     // Attempt to read and parse
     let read_result = ({
         use std::io::Read;
-        std::fs::File::open(base.join(".jk/attestation/0001.json")).and_then(|mut f| {
+        std::fs::File::open(base.join(".jk/attestation/0001.json")).and_then(|f| {
             let mut buf = String::new();
             f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
             Ok(buf)
diff --git a/crates/januskey-cli/tests/p2p_test.rs b/crates/januskey-cli/tests/p2p_test.rs
index 7a5265c..e2a252d 100644
--- a/crates/januskey-cli/tests/p2p_test.rs
+++ b/crates/januskey-cli/tests/p2p_test.rs
@@ -103,7 +103,7 @@ fn key_operation_creates_attestation_entry() {
     // Verify attestation references the key
     let read_back = ({
         use std::io::Read;
-        std::fs::File::open(attest_path.join("0001.json")).and_then(|mut f| {
+        std::fs::File::open(attest_path.join("0001.json")).and_then(|f| {
             let mut buf = String::new();
             f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
             Ok(buf)
@@ -143,7 +143,7 @@ fn attestation_chain_integrity() {
         .map(|i| {
             ({
                 use std::io::Read;
-                std::fs::File::open(attest_path.join(format!("{:04}.json", i))).and_then(|mut f| {
+                std::fs::File::open(attest_path.join(format!("{:04}.json", i))).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
@@ -195,11 +195,7 @@ fn transaction_groups_operations() {
     let op_files: Vec<_> = std::fs::read_dir(&ops_path)
         .unwrap()
         .filter_map(|e| e.ok())
-        .filter(|e| {
-            e.file_name()
-                .to_str()
-                .map_or(false, |n| n.starts_with(tx_id))
-        })
+        .filter(|e| e.file_name().to_str().is_some_and(|n| n.starts_with(tx_id)))
         .collect();
     assert_eq!(op_files.len(), 3, "Transaction must group all 3 operations");
 }
diff --git a/crates/reversible-core/src/manifest.rs b/crates/reversible-core/src/manifest.rs
index 28799e8..26503a7 100644
--- a/crates/reversible-core/src/manifest.rs
+++ b/crates/reversible-core/src/manifest.rs
@@ -41,7 +41,7 @@ impl ManifestEmitter {
 
         // Header
         manifest.push_str("@manifest\n");
-        manifest.push_str(&format!("  version = \"1.0\"\n"));
+        manifest.push_str("  version = \"1.0\"\n");
         manifest.push_str(&format!("  subsystem = \"{}\"\n", subsystem));
         manifest.push_str(&format!("  timestamp = \"{}\"\n", timestamp));
         manifest.push_str(&format!(
@@ -105,7 +105,7 @@ impl ManifestEmitter {
             };
 
             let current = hasher.finalize_reset();
-            hasher.update(&current);
+            hasher.update(current);
             hasher.update(&op_hash);
         }
 
diff --git a/crates/reversible-core/src/metadata.rs b/crates/reversible-core/src/metadata.rs
index 7beb3a2..fe44d8a 100644
--- a/crates/reversible-core/src/metadata.rs
+++ b/crates/reversible-core/src/metadata.rs
@@ -263,7 +263,7 @@ impl MetadataStore {
         let log = if path.exists() {
             let content = ({
                 use std::io::Read;
-                std::fs::File::open(&path).and_then(|mut f| {
+                std::fs::File::open(&path).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)
diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs
index 2f0ff6c..8f47601 100644
--- a/crates/reversible-core/src/transaction.rs
+++ b/crates/reversible-core/src/transaction.rs
@@ -123,7 +123,7 @@ impl TransactionManager {
         let log = if path.exists() {
             let content = ({
                 use std::io::Read;
-                std::fs::File::open(&path).and_then(|mut f| {
+                std::fs::File::open(&path).and_then(|f| {
                     let mut buf = String::new();
                     f.take(10 * 1024 * 1024).read_to_string(&mut buf)?;
                     Ok(buf)

From e6fee6739ca8eb2d41f8fea3963b35a3a1941954 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 2 Oct 2026 13:51:28 +0100
Subject: [PATCH 2/4] fix(ci): give every e2e.yml Rust job a toolchain; aspect
 docs accept .adoc

- dtolnay/rust-toolchain@v1 needs a `toolchain` input; the Criterion,
  E2E Lifecycle and Panic Attack jobs had none ("'toolchain' is a required
  input"). Set `stable`.
- tests/aspect: SECURITY/ARCHITECTURE/PROOF-NEEDS/TOPOLOGY were migrated
  to .adoc, so the .md-only existence checks failed 4/29. Accept either,
  as README already did. Negative control: removing TOPOLOGY.adoc makes
  the check FAIL.
- attestation: propagate HMAC new_from_slice's error instead of expect()
  (Hypatia expect_in_hot_path; the fn already returns io::Result).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
---
 .github/workflows/e2e.yml              | 6 ++++++
 crates/januskey-cli/src/attestation.rs | 3 +--
 tests/aspect/cross_cutting_test.sh     | 8 ++++----
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index 3e23f5c..629758a 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -40,6 +40,8 @@ jobs:
     steps:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
+        with:
+          toolchain: stable
       - uses: Swatinem/rust-cache@v2.9.2
       - name: Run benchmarks
         run: cargo bench -- --output-format bencher 2>/dev/null || echo "Benchmarks completed"
@@ -51,6 +53,8 @@ jobs:
     steps:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
+        with:
+          toolchain: stable
       - uses: Swatinem/rust-cache@v2.9.2
       - name: Build release
         run: cargo build --release
@@ -90,6 +94,8 @@ jobs:
     steps:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
+        with:
+          toolchain: stable
       - name: Install panic-attack
         run: cargo install --git https://github.com/hyperpolymath/panic-attacker.git 2>/dev/null || echo "panic-attack unavailable"
       - name: Run assail scan
diff --git a/crates/januskey-cli/src/attestation.rs b/crates/januskey-cli/src/attestation.rs
index 08e54d3..1711955 100644
--- a/crates/januskey-cli/src/attestation.rs
+++ b/crates/januskey-cli/src/attestation.rs
@@ -209,8 +209,7 @@ impl AuditLog {
             )
         })?;
 
-        let mut mac =
-            <Hmac<Sha256>>::new_from_slice(&key).expect("HMAC accepts keys of any length");
+        let mut mac = <Hmac<Sha256>>::new_from_slice(&key).map_err(std::io::Error::other)?;
         mac.update(Self::ATTESTATION_SCHEME.as_bytes());
         mac.update(b"\x00");
         mac.update(data.as_bytes());
diff --git a/tests/aspect/cross_cutting_test.sh b/tests/aspect/cross_cutting_test.sh
index 37cd574..7b3599f 100755
--- a/tests/aspect/cross_cutting_test.sh
+++ b/tests/aspect/cross_cutting_test.sh
@@ -52,10 +52,10 @@ check "No unsafe in reversible-core" "! grep -rh 'unsafe' '${JK_DIR}/crates/reve
 # --- Documentation ---
 echo "--- Documentation ---"
 check "README exists" "[ -f '${JK_DIR}/README.md' ] || [ -f '${JK_DIR}/README.adoc' ]"
-check "SECURITY.md exists" "[ -f '${JK_DIR}/SECURITY.md' ]"
-check "ARCHITECTURE.md exists" "[ -f '${JK_DIR}/ARCHITECTURE.md' ]"
-check "PROOF-NEEDS.md exists" "[ -f '${JK_DIR}/PROOF-NEEDS.md' ]"
-check "TOPOLOGY.md exists" "[ -f '${JK_DIR}/TOPOLOGY.md' ]"
+check "SECURITY exists" "[ -f '${JK_DIR}/SECURITY.md' ] || [ -f '${JK_DIR}/SECURITY.adoc' ]"
+check "ARCHITECTURE exists" "[ -f '${JK_DIR}/ARCHITECTURE.md' ] || [ -f '${JK_DIR}/ARCHITECTURE.adoc' ]"
+check "PROOF-NEEDS exists" "[ -f '${JK_DIR}/PROOF-NEEDS.md' ] || [ -f '${JK_DIR}/PROOF-NEEDS.adoc' ]"
+check "TOPOLOGY exists" "[ -f '${JK_DIR}/TOPOLOGY.md' ] || [ -f '${JK_DIR}/TOPOLOGY.adoc' ]"
 check "LICENSE directory exists" "[ -d '${JK_DIR}/LICENSES' ]"
 
 # --- Proofs ---

From 6f31e8982a267f34a8f7e24fa3d017b2f97ddda2 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 2 Oct 2026 14:02:02 +0100
Subject: [PATCH 3/4] feat(dashboard-check): claims ledger, run every TESTED
 row, reconcile counts

ULTRAPLAN P1-0, first of three stacked PRs.

PROOF-NEEDS.adoc gains a `=== Claims ledger` table, one row per line:
claim | status | artefact | command, status one of PROVEN / TESTED /
ASSUMED / DESIGNED / OPEN. dashboard-check now:

- rejects a wrapped row, an unknown status, a missing table, naming the line;
- for TESTED rows, requires the artefact file to name the test, the command
  to exit 0, and an output line showing that test passing, so `true` or a
  filter that runs 0 tests fails;
- for PROVEN rows, requires the theorem name and a passing checker command;
- for ASSUMED / DESIGNED / OPEN, requires command `-` and an existing file
  or #N artefact;
- measures tests with `cargo test --workspace --locked -- --list` and fails
  when README / EXPLAINME / TOPOLOGY / READINESS print a different test
  count, or a proof count different from the number of PROVEN rows.

The ledger has 7 TESTED rows and 2 OPEN rows (#145); 0 PROVEN, because
the Idris2 ABI does not typecheck. The dashboards claimed 67 tests and
30 proofs; they now say 119 tests and 0 checked proofs.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
---
 PROOF-NEEDS.adoc                     |  29 ++
 READINESS.adoc                       |   8 +-
 TOPOLOGY.adoc                        |   6 +-
 crates/dashboard-check/src/claims.rs | 536 +++++++++++++++++++++++++++
 crates/dashboard-check/src/main.rs   |  50 ++-
 5 files changed, 621 insertions(+), 8 deletions(-)
 create mode 100644 crates/dashboard-check/src/claims.rs

diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index b471398..9f60ff6 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -45,6 +45,35 @@ content |Hash collisions or bugs corrupt stored data
 januskey-cli
 |===
 
+=== Claims ledger
+
+Every claim JanusKey makes about its own correctness is a row here, with one
+of five statuses: PROVEN (a checker accepts a proof), TESTED (a named test
+passes), ASSUMED (relied on, not checked), DESIGNED (specified, not built) or
+OPEN (not true yet). `cargo run -p dashboard-check -- --check .` runs the
+command of every PROVEN and TESTED row and fails unless it exits 0 and, for
+TESTED, prints the named test passing. The counts on README, EXPLAINME,
+TOPOLOGY and READINESS must equal what that checker measures: tests by
+`cargo test --workspace --locked -- --list`, proofs by the PROVEN rows below.
+Each row is one line; the checker rejects a wrapped row.
+
+There are no PROVEN rows: the Idris2 ABI does not typecheck (#145), so no
+proof in this repository is checked by anything.
+
+[cols="3,1,3,3",options="header"]
+|===
+|Claim |Status |Artefact |Command
+|Obliterating a path shreds its unshared blobs and log entries, and undo then has nothing |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::obliterate_scrubs_blobs_log_and_undo` |`cargo test --locked -p januskey --test obliteration_cas_test obliterate_scrubs_blobs_log_and_undo`
+|Obliteration keeps a blob another path still references |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::obliterate_keeps_blob_shared_with_another_path` |`cargo test --locked -p januskey --test obliteration_cas_test obliterate_keeps_blob_shared_with_another_path`
+|`jk obliterate` scrubs the store end to end through the CLI |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::cli_obliterate_scrubs_store_and_undo_has_nothing` |`cargo test --locked -p januskey --test obliteration_cas_test cli_obliterate_scrubs_store_and_undo_has_nothing`
+|Execute then undo restores the prior state (property test over generated ops) |TESTED |`crates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity` |`cargo test --locked -p januskey --test property_tests execute_then_undo_is_identity`
+|Content store round-trips arbitrary bytes (property test) |TESTED |`crates/reversible-core/tests/property_tests.rs::content_store_roundtrip` |`cargo test --locked -p reversible-core --test property_tests content_store_roundtrip`
+|A transaction rolled back ends RolledBack with none active (property test) |TESTED |`crates/reversible-core/tests/property_tests.rs::transaction_begin_rollback_roundtrip` |`cargo test --locked -p reversible-core --test property_tests transaction_begin_rollback_roundtrip`
+|The audit log verifies an untampered three-entry chain as valid (tamper detection is not tested) |TESTED |`crates/januskey-cli/src/attestation.rs::test_audit_log_chain_integrity` |`cargo test --locked -p januskey --lib test_audit_log_chain_integrity`
+|The Idris2 ABI typechecks and its six security claims are proved |OPEN |#145 |-
+|Every operation is reversible (MPR), as a theorem linked to the Rust |OPEN |#145 |-
+|===
+
 === Recommended Prover
 
 *Idris2* — Create `+src/abi/+` with dependent type proofs for
diff --git a/READINESS.adoc b/READINESS.adoc
index 0acb094..7cd3c63 100644
--- a/READINESS.adoc
+++ b/READINESS.adoc
@@ -8,8 +8,8 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 
 === CRG Grade: D (Alpha — Unstable)
 
-*Justification:* Tests exist and pass (67 total), proofs exist (30
-Idris2, unchecked in CI), benchmarks exist (5 Criterion groups). But: no
+*Justification:* 119 tests pass (`cargo test --workspace --locked -- --list`); the
+Idris2 ABI does not typecheck, so 0 proofs are checked (#145); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips,
 benchmarks measured fake crypto until this session. RSR compliance
 present. Deep annotation incomplete (TOPOLOGY.md exists but
@@ -60,11 +60,11 @@ handling
 
 |15 |Compatibility |MISSING |0 |— |No version migration tests
 
-|16 |Proof regression |✓ |30 proofs |`+just test-proofs+` |Idris2 –check
+|16 |Proof regression |✗ |0 checked (#145) |`+just test-proofs+` |Idris2 –check
 (requires idris2 binary)
 |===
 
-*Total passing:* 67 tests + 5 benchmark groups + 30 Idris2 proofs *Total
+*Total passing:* 119 tests + 5 benchmark groups; 0 Idris2 proofs checked (#145) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix
diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc
index 7324c95..fecd46f 100644
--- a/TOPOLOGY.adoc
+++ b/TOPOLOGY.adoc
@@ -1,5 +1,5 @@
 == JanusKey — Project Topology
-// Last updated: 2026-07-02 (completion dashboard reconciled to STATE.a2ml / READINESS; date carried over from TOPOLOGY.md, dropped by the md-to-adoc migration #102)
+// Last updated: 2026-10-02 (test and proof counts reconciled to the PROOF-NEEDS claims ledger by dashboard-check)
 
 === System Architecture
 
@@ -77,9 +77,9 @@ SECURITY (honest)
 INTERFACES & RESEARCH
   CLI Interface (jk)                ████████░░  ~85%   Full command set; no user testing yet
   MPR Methodology                   ████░░░░░░  ~40%   Design documented; FORMAL PROOFS PENDING
-                                                        (30 Idris2 proofs unchecked in CI; not linked
+                                                        (Idris2 ABI does not typecheck, #145; 0 proofs checked; not linked
                                                         to the Rust)
-  Testing (READINESS matrix)        ██████░░░░  ~60%   67 tests + 5 benches; missing fuzz, mutation,
+  Testing (READINESS matrix)        ██████░░░░  ~60%   119 tests + 5 benches; missing fuzz, mutation,
                                                         chaos, compatibility (Grade D)
 
 REPO INFRASTRUCTURE
diff --git a/crates/dashboard-check/src/claims.rs b/crates/dashboard-check/src/claims.rs
new file mode 100644
index 0000000..f4139e1
--- /dev/null
+++ b/crates/dashboard-check/src/claims.rs
@@ -0,0 +1,536 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+//
+// Claims ledger (ULTRAPLAN P1-0): every claim the repo makes about itself is a
+// row `claim | status | artefact | command` in the `=== Claims ledger` table of
+// PROOF-NEEDS.adoc. Status is one of PROVEN / TESTED / ASSUMED / DESIGNED /
+// OPEN. This module checks that each row is discharged by its artefact, and
+// that the counts printed on the dashboards equal what was measured.
+//
+// Rules, each of which has a fixture below:
+// - One row per line. A row that wraps onto a second line is rejected,
+//   because a parser that guesses where a wrapped row ends can be lied to.
+// - TESTED: the artefact is `<file>::<test path>`. The file must exist and
+//   name the test, the command must exit 0, and some output line must name the
+//   test and say `ok` or `PASS`. A command that runs nothing (a filter that
+//   matches no test, or plain `true`) therefore fails.
+// - PROVEN: the artefact is `<file>::<theorem>`. The file must exist and name
+//   the theorem, and the command (the checker run) must exit 0.
+// - ASSUMED / DESIGNED / OPEN: nothing is run, so the command cell must be `-`.
+//   The artefact must be an existing file or an issue reference `#N`.
+// - Dashboard counts: a number followed (within two words) by "test(s)" must
+//   equal the measured test count; one followed by "proof(s)" or "theorem(s)"
+//   must equal the number of PROVEN rows.
+
+use std::path::Path;
+use std::process::Command;
+
+/// The five statuses a claim may carry.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Status {
+    Proven,
+    Tested,
+    Assumed,
+    Designed,
+    Open,
+}
+
+impl Status {
+    /// Parse a status cell; `None` for anything outside the taxonomy.
+    fn parse(cell: &str) -> Option<Status> {
+        match cell {
+            "PROVEN" => Some(Status::Proven),
+            "TESTED" => Some(Status::Tested),
+            "ASSUMED" => Some(Status::Assumed),
+            "DESIGNED" => Some(Status::Designed),
+            "OPEN" => Some(Status::Open),
+            _ => None,
+        }
+    }
+}
+
+/// One ledger row, with the PROOF-NEEDS line it came from for error messages.
+#[derive(Debug, Clone, PartialEq)]
+pub struct Claim {
+    pub line: usize,
+    pub claim: String,
+    pub status: Status,
+    pub artefact: String,
+    pub command: String,
+}
+
+/// Strip AsciiDoc inline-literal markup (`` `x` `` or `` `+x+` ``) from a cell.
+fn unliteral(cell: &str) -> String {
+    let c = cell.trim();
+    let c = c
+        .strip_prefix('`')
+        .and_then(|s| s.strip_suffix('`'))
+        .unwrap_or(c);
+    let c = c
+        .strip_prefix('+')
+        .and_then(|s| s.strip_suffix('+'))
+        .unwrap_or(c);
+    c.trim().to_string()
+}
+
+/// Parse the `=== Claims ledger` table out of PROOF-NEEDS.adoc. Errors name
+/// the offending line; a missing section or table is an error, not an empty
+/// ledger.
+pub fn parse_ledger(src: &str) -> Result<Vec<Claim>, Vec<String>> {
+    let lines: Vec<&str> = src.lines().collect();
+    let Some(heading) = lines.iter().position(|l| l.trim() == "=== Claims ledger") else {
+        return Err(vec![
+            "PROOF-NEEDS.adoc has no '=== Claims ledger' section".into()
+        ]);
+    };
+    let Some(open) = lines[heading..]
+        .iter()
+        .position(|l| l.trim() == "|===")
+        .map(|i| heading + i)
+    else {
+        return Err(vec!["'=== Claims ledger' has no |=== table".into()]);
+    };
+
+    let mut claims = Vec::new();
+    let mut errors = Vec::new();
+    let mut header_seen = false;
+    let mut closed = false;
+    for (i, raw) in lines.iter().enumerate().skip(open + 1) {
+        let n = i + 1;
+        let l = raw.trim();
+        if l == "|===" {
+            closed = true;
+            break;
+        }
+        if l.is_empty() {
+            continue;
+        }
+        let Some(body) = l.strip_prefix('|') else {
+            errors.push(format!(
+                "PROOF-NEEDS.adoc:{n}: ledger rows must fit on one line starting with '|' (wrapped row?)"
+            ));
+            continue;
+        };
+        let cells: Vec<String> = body.split('|').map(unliteral).collect();
+        if cells.len() != 4 {
+            errors.push(format!(
+                "PROOF-NEEDS.adoc:{n}: expected 4 cells (claim | status | artefact | command), found {}",
+                cells.len()
+            ));
+            continue;
+        }
+        if !header_seen {
+            header_seen = true;
+            continue;
+        }
+        let Some(status) = Status::parse(&cells[1]) else {
+            errors.push(format!(
+                "PROOF-NEEDS.adoc:{n}: status '{}' is not PROVEN / TESTED / ASSUMED / DESIGNED / OPEN",
+                cells[1]
+            ));
+            continue;
+        };
+        claims.push(Claim {
+            line: n,
+            claim: cells[0].clone(),
+            status,
+            artefact: cells[2].clone(),
+            command: cells[3].clone(),
+        });
+    }
+    if !closed {
+        errors.push("the claims ledger table is not closed with |===".into());
+    }
+    if errors.is_empty() && claims.is_empty() {
+        errors.push("the claims ledger has no rows".into());
+    }
+    if errors.is_empty() {
+        Ok(claims)
+    } else {
+        Err(errors)
+    }
+}
+
+/// True when `needle` occurs in `hay` with no identifier character on either
+/// side, so `foo` does not match inside `foo_bar` or `xfoo`.
+fn contains_word(hay: &str, needle: &str) -> bool {
+    let is_ident = |c: char| c.is_ascii_alphanumeric() || c == '_';
+    hay.match_indices(needle).any(|(i, _)| {
+        let before = hay[..i].chars().next_back();
+        let after = hay[i + needle.len()..].chars().next();
+        !before.is_some_and(is_ident) && !after.is_some_and(is_ident)
+    })
+}
+
+/// Split a `<file>::<name>` artefact; `None` if it has no `::`.
+fn split_artefact(artefact: &str) -> Option<(&str, &str)> {
+    artefact
+        .split_once("::")
+        .filter(|(f, n)| !f.is_empty() && !n.is_empty())
+}
+
+/// Check that the artefact file exists under `root` and names the last
+/// `::` segment of `name` as a whole word.
+fn artefact_present(root: &Path, file: &str, name: &str) -> Result<(), String> {
+    let leaf = name.rsplit("::").next().unwrap_or(name);
+    let text = std::fs::read_to_string(root.join(file))
+        .map_err(|e| format!("artefact file {file} cannot be read: {e}"))?;
+    if contains_word(&text, leaf) {
+        Ok(())
+    } else {
+        Err(format!("artefact file {file} does not mention '{leaf}'"))
+    }
+}
+
+/// Run a ledger command with `sh -c` in `root`. Returns whether it exited 0
+/// and its combined stdout and stderr. Failing to start is an error.
+pub fn run_command(root: &Path, command: &str) -> Result<(bool, String), String> {
+    let out = Command::new("sh")
+        .arg("-c")
+        .arg(command)
+        .current_dir(root)
+        .output()
+        .map_err(|e| format!("cannot start `{command}`: {e}"))?;
+    let mut text = String::from_utf8_lossy(&out.stdout).into_owned();
+    text.push_str(&String::from_utf8_lossy(&out.stderr));
+    Ok((out.status.success(), text))
+}
+
+/// True when some output line names the test and reports it passed
+/// (`test <name> ... ok` from libtest, `[PASS] <name>` from shell harnesses).
+fn output_shows_pass(output: &str, name: &str) -> bool {
+    output
+        .lines()
+        .any(|l| contains_word(l, name) && (contains_word(l, "ok") || contains_word(l, "PASS")))
+}
+
+/// Check one claim against its artefact, running its command when the status
+/// requires it. `run` is injected so the rules can be tested without cargo.
+pub fn check_claim<F>(root: &Path, c: &Claim, run: &F) -> Result<(), String>
+where
+    F: Fn(&Path, &str) -> Result<(bool, String), String>,
+{
+    let at = format!("PROOF-NEEDS.adoc:{} ({})", c.line, c.claim);
+    match c.status {
+        Status::Tested | Status::Proven => {
+            let (file, name) = split_artefact(&c.artefact)
+                .ok_or_else(|| format!("{at}: artefact '{}' must be <file>::<name>", c.artefact))?;
+            artefact_present(root, file, name).map_err(|e| format!("{at}: {e}"))?;
+            if c.command.is_empty() || c.command == "-" {
+                return Err(format!("{at}: a {:?} claim needs a command", c.status));
+            }
+            let (ok, output) = run(root, &c.command).map_err(|e| format!("{at}: {e}"))?;
+            if !ok {
+                return Err(format!("{at}: `{}` failed", c.command));
+            }
+            if c.status == Status::Tested && !output_shows_pass(&output, name) {
+                return Err(format!(
+                    "{at}: `{}` exited 0 but no output line shows '{name}' passing (did it run the test at all?)",
+                    c.command
+                ));
+            }
+            Ok(())
+        }
+        Status::Assumed | Status::Designed | Status::Open => {
+            if c.command != "-" {
+                return Err(format!(
+                    "{at}: a {:?} claim runs nothing, so its command cell must be '-'",
+                    c.status
+                ));
+            }
+            let a = c.artefact.as_str();
+            let is_issue = a
+                .strip_prefix('#')
+                .is_some_and(|n| !n.is_empty() && n.bytes().all(|b| b.is_ascii_digit()));
+            let file = split_artefact(a).map_or(a, |(f, _)| f);
+            if is_issue || root.join(file).is_file() {
+                Ok(())
+            } else {
+                Err(format!(
+                    "{at}: artefact '{a}' is neither an existing file nor an issue reference #N"
+                ))
+            }
+        }
+    }
+}
+
+/// What a dashboard number counts.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum CountKind {
+    Tests,
+    Proofs,
+}
+
+/// Find `<number> [word] tests|proofs|theorems` claims in a dashboard. A
+/// number must be a token of its own, so `Idris2 proofs` is not a claim of 2.
+pub fn scan_counts(text: &str) -> Vec<(usize, u64, CountKind)> {
+    let norm = |t: &str| -> String {
+        t.trim_matches(|c: char| !c.is_ascii_alphanumeric())
+            .to_ascii_lowercase()
+    };
+    let kind = |w: &str| match w {
+        "test" | "tests" => Some(CountKind::Tests),
+        "proof" | "proofs" | "theorem" | "theorems" => Some(CountKind::Proofs),
+        _ => None,
+    };
+    let mut found = Vec::new();
+    for (i, line) in text.lines().enumerate() {
+        // Table cells are scanned separately, so a row number in one cell
+        // cannot pair with a "Proof …" heading in the next.
+        for cell in line.split('|') {
+            // A percentage is not a count, so `%` tokens are blanked out.
+            let toks: Vec<String> = cell
+                .split_whitespace()
+                .map(|t| {
+                    if t.contains('%') {
+                        String::new()
+                    } else {
+                        norm(t)
+                    }
+                })
+                .collect();
+            let is_num = |t: &str| !t.is_empty() && t.bytes().all(|b| b.is_ascii_digit());
+            for (j, t) in toks.iter().enumerate() {
+                if !is_num(t) {
+                    continue;
+                }
+                let Ok(n) = t.parse::<u64>() else { continue };
+                // Look at most two words ahead, stopping at the next number.
+                let k = toks[j + 1..]
+                    .iter()
+                    .take(2)
+                    .take_while(|w| !is_num(w))
+                    .find_map(|w| kind(w));
+                if let Some(k) = k {
+                    found.push((i + 1, n, k));
+                }
+            }
+        }
+    }
+    found
+}
+
+/// Compare every count on a dashboard with the measured values.
+pub fn check_counts(
+    surface: &str,
+    text: &str,
+    measured_tests: u64,
+    proven_rows: u64,
+) -> Vec<String> {
+    scan_counts(text)
+        .into_iter()
+        .filter_map(|(line, n, k)| {
+            let (want, what) = match k {
+                CountKind::Tests => (
+                    measured_tests,
+                    "tests measured by `cargo test --workspace --locked -- --list`",
+                ),
+                CountKind::Proofs => (proven_rows, "PROVEN rows in the claims ledger"),
+            };
+            (n != want).then(|| format!("{surface}:{line}: claims {n} but there are {want} {what}"))
+        })
+        .collect()
+}
+
+/// Count the workspace's tests: the lines of `cargo test --workspace --locked
+/// -- --list` that end in `: test`. Zero is an error, since a workspace with
+/// tests that lists none means the instrument failed.
+pub fn measure_tests(root: &Path) -> Result<u64, String> {
+    let out = Command::new("cargo")
+        .args(["test", "--workspace", "--locked", "--", "--list"])
+        .current_dir(root)
+        .output()
+        .map_err(|e| format!("cannot run cargo to measure the test count: {e}"))?;
+    if !out.status.success() {
+        return Err(format!(
+            "`cargo test --workspace --locked -- --list` failed:\n{}",
+            String::from_utf8_lossy(&out.stderr)
+        ));
+    }
+    let n = String::from_utf8_lossy(&out.stdout)
+        .lines()
+        .filter(|l| l.ends_with(": test"))
+        .count() as u64;
+    if n == 0 {
+        return Err(
+            "`cargo test -- --list` listed 0 tests; refusing to treat that as a measurement".into(),
+        );
+    }
+    Ok(n)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    const LEDGER: &str = "\
+=== Claims ledger
+
+[cols=\"3,1,3,3\",options=\"header\"]
+|===
+|Claim |Status |Artefact |Command
+|Undo restores content |TESTED |`src/a.rs::undo_restores` |`cargo test undo_restores`
+|Attestation is unforgeable |OPEN |#145 |-
+|===
+";
+
+    /// A fake runner that returns a fixed exit status and output.
+    fn fake(ok: bool, out: &'static str) -> impl Fn(&Path, &str) -> Result<(bool, String), String> {
+        move |_: &Path, _: &str| Ok((ok, out.to_string()))
+    }
+
+    /// A temp dir holding `src/a.rs` with a test named `undo_restores`.
+    fn repo(tag: &str) -> std::path::PathBuf {
+        let d = std::env::temp_dir().join(format!("claims-{tag}-{}", std::process::id()));
+        std::fs::create_dir_all(d.join("src")).unwrap();
+        std::fs::write(d.join("src/a.rs"), "#[test]\nfn undo_restores() {}\n").unwrap();
+        d
+    }
+
+    /// The TESTED row of [`LEDGER`].
+    fn tested_row() -> Claim {
+        parse_ledger(LEDGER).unwrap().remove(0)
+    }
+
+    #[test]
+    fn parses_rows_and_strips_literals() {
+        let c = parse_ledger(LEDGER).unwrap();
+        assert_eq!(c.len(), 2);
+        assert_eq!(c[0].status, Status::Tested);
+        assert_eq!(c[0].artefact, "src/a.rs::undo_restores");
+        assert_eq!(c[0].command, "cargo test undo_restores");
+        assert_eq!(c[1].status, Status::Open);
+    }
+
+    #[test]
+    fn wrapped_row_is_rejected() {
+        let wrapped = LEDGER.replace(
+            "|`cargo test undo_restores`",
+            "\n`cargo test undo_restores`",
+        );
+        let e = parse_ledger(&wrapped).unwrap_err();
+        assert!(e.iter().any(|e| e.contains("wrapped row")), "{e:?}");
+    }
+
+    #[test]
+    fn unknown_status_and_missing_section_are_rejected() {
+        let e = parse_ledger(&LEDGER.replace("|OPEN |", "|DONE |")).unwrap_err();
+        assert!(e.iter().any(|e| e.contains("'DONE'")), "{e:?}");
+        assert!(parse_ledger("= nothing here\n").is_err());
+    }
+
+    #[test]
+    fn tested_row_passes_when_output_shows_the_test() {
+        let d = repo("pass");
+        let r = check_claim(
+            &d,
+            &tested_row(),
+            &fake(true, "test undo_restores ... ok\n"),
+        );
+        std::fs::remove_dir_all(&d).unwrap();
+        assert_eq!(r, Ok(()));
+    }
+
+    // PROVEN needs the theorem in the file and a passing checker run; unlike
+    // TESTED it needs no per-name output, since provers print nothing on success.
+    #[test]
+    fn proven_row_needs_theorem_and_passing_checker() {
+        let d = repo("proven");
+        std::fs::write(
+            d.join("src/P.idr"),
+            "undoInverse : (x : S) -> undo (op x) = x\n",
+        )
+        .unwrap();
+        let mut c = tested_row();
+        c.status = Status::Proven;
+        c.artefact = "src/P.idr::undoInverse".into();
+        c.command = "idris2 --check src/P.idr".into();
+        let ok = check_claim(&d, &c, &fake(true, ""));
+        let rejected = check_claim(&d, &c, &fake(false, "error"));
+        c.artefact = "src/P.idr::undoInverseAll".into();
+        let absent = check_claim(&d, &c, &fake(true, ""));
+        std::fs::remove_dir_all(&d).unwrap();
+        assert_eq!(ok, Ok(()));
+        assert!(rejected.unwrap_err().contains("failed"));
+        assert!(absent.unwrap_err().contains("does not mention"));
+    }
+
+    // LyingVerifier: the command exits 0 but never ran the test.
+    #[test]
+    fn lying_verifier_fails() {
+        let d = repo("liar");
+        let r = check_claim(&d, &tested_row(), &fake(true, ""));
+        std::fs::remove_dir_all(&d).unwrap();
+        assert!(r.unwrap_err().contains("no output line shows"));
+    }
+
+    // UncheckedSkip: a filter that matches nothing is `running 0 tests`, rc 0.
+    #[test]
+    fn unchecked_skip_fails() {
+        let d = repo("skip");
+        let out = "running 0 tests\n\ntest result: ok. 0 passed; 0 failed\n";
+        let r = check_claim(&d, &tested_row(), &fake(true, out));
+        std::fs::remove_dir_all(&d).unwrap();
+        assert!(r.unwrap_err().contains("no output line shows"));
+    }
+
+    #[test]
+    fn failing_command_and_missing_artefact_fail() {
+        let d = repo("fail");
+        let failed = check_claim(&d, &tested_row(), &fake(false, "test undo_restores ... ok"));
+        let mut gone = tested_row();
+        gone.artefact = "src/a.rs::no_such_test".into();
+        let absent = check_claim(&d, &gone, &fake(true, "test no_such_test ... ok"));
+        std::fs::remove_dir_all(&d).unwrap();
+        assert!(failed.unwrap_err().contains("failed"));
+        assert!(absent.unwrap_err().contains("does not mention"));
+    }
+
+    #[test]
+    fn real_shell_runner_reports_status_and_output() {
+        let d = std::env::temp_dir();
+        assert_eq!(run_command(&d, "echo hi").unwrap(), (true, "hi\n".into()));
+        assert!(!run_command(&d, "exit 3").unwrap().0);
+    }
+
+    #[test]
+    fn open_rows_run_nothing_and_need_a_real_artefact() {
+        let d = repo("open");
+        let mut c = parse_ledger(LEDGER).unwrap().remove(1);
+        let ok = check_claim(&d, &c, &fake(false, ""));
+        c.command = "cargo test".into();
+        let ran = check_claim(&d, &c, &fake(true, ""));
+        c.command = "-".into();
+        c.artefact = "docs/missing.adoc".into();
+        let missing = check_claim(&d, &c, &fake(true, ""));
+        std::fs::remove_dir_all(&d).unwrap();
+        assert_eq!(ok, Ok(()));
+        assert!(ran.unwrap_err().contains("must be '-'"));
+        assert!(missing.unwrap_err().contains("neither an existing file"));
+    }
+
+    #[test]
+    fn scans_counts_but_not_digits_inside_words() {
+        let t = "67 tests + 5 benchmark groups + 30 Idris2 proofs\nIdris2 proofs not checked\n";
+        assert_eq!(
+            scan_counts(t),
+            vec![(1, 67, CountKind::Tests), (1, 30, CountKind::Proofs)]
+        );
+        assert!(scan_counts("|16 |Proof regression |✓ |`just test-proofs`").is_empty());
+    }
+
+    // Inflated count: the dashboard says 67, the instrument measured 107.
+    #[test]
+    fn inflated_counts_fail_and_true_counts_pass() {
+        let p = check_counts(
+            "TOPOLOGY.adoc",
+            "~60%   67 tests + 5 benches\n30 Idris2 proofs\n",
+            107,
+            0,
+        );
+        assert_eq!(p.len(), 2, "{p:?}");
+        assert!(p[0].contains("TOPOLOGY.adoc:1: claims 67 but there are 107"));
+        assert!(p[1].contains("claims 30 but there are 0 PROVEN rows"));
+        assert!(check_counts("T", "107 tests; 0 Idris2 proofs PROVEN\n", 107, 0).is_empty());
+    }
+}
diff --git a/crates/dashboard-check/src/main.rs b/crates/dashboard-check/src/main.rs
index 4bc9d2c..db0c90f 100644
--- a/crates/dashboard-check/src/main.rs
+++ b/crates/dashboard-check/src/main.rs
@@ -23,6 +23,8 @@
 // Exits 0 only if every reconciled field was found and agrees with STATE;
 // non-zero with a report otherwise. `--check` is the default and only mode.
 
+mod claims;
+
 use std::path::{Path, PathBuf};
 use std::process::ExitCode;
 
@@ -299,6 +301,51 @@ fn check_grade(
     }
 }
 
+/// Check the claims ledger in PROOF-NEEDS (ULTRAPLAN P1-0): run every PROVEN
+/// and TESTED row, then compare the counts printed on the dashboards with the
+/// measured test count and the number of PROVEN rows.
+fn check_claims(root: &Path, r: &mut Report) {
+    let Some(ledger) = read_surface(root, "PROOF-NEEDS") else {
+        r.problems
+            .push("no PROOF-NEEDS.adoc or PROOF-NEEDS.md holding the claims ledger".into());
+        return;
+    };
+    let claims = match claims::parse_ledger(&ledger.text) {
+        Ok(c) => c,
+        Err(errors) => {
+            r.problems.extend(errors);
+            return;
+        }
+    };
+    for c in &claims {
+        match claims::check_claim(root, c, &claims::run_command) {
+            Ok(()) => r
+                .observed
+                .push(format!("{:?}: {} ({})", c.status, c.claim, c.artefact)),
+            Err(e) => r.problems.push(e),
+        }
+    }
+    let proven = claims
+        .iter()
+        .filter(|c| c.status == claims::Status::Proven)
+        .count() as u64;
+    let tests = match claims::measure_tests(root) {
+        Ok(n) => n,
+        Err(e) => {
+            r.problems.push(e);
+            return;
+        }
+    };
+    r.observed
+        .push(format!("{tests} tests measured, {proven} PROVEN claims"));
+    for stem in ["README", "EXPLAINME", "TOPOLOGY", "READINESS"] {
+        if let Some(s) = read_surface(root, stem) {
+            r.problems
+                .extend(claims::check_counts(&s.name, &s.text, tests, proven));
+        }
+    }
+}
+
 /// Read a file to a string, `None` if it is absent or unreadable.
 fn read_opt(path: &Path) -> Option<String> {
     std::fs::read_to_string(path).ok()
@@ -336,7 +383,8 @@ fn main() -> ExitCode {
     let topology = read_surface(&root, "TOPOLOGY");
     let readiness = read_surface(&root, "READINESS");
 
-    let report = reconcile(&state, topology.as_ref(), readiness.as_ref());
+    let mut report = reconcile(&state, topology.as_ref(), readiness.as_ref());
+    check_claims(&root, &mut report);
 
     if report.problems.is_empty() {
         println!(

From 274883ae624c7ecf5209b72fe426dec6d94036d8 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Fri, 2 Oct 2026 14:06:43 +0100
Subject: [PATCH 4/4] docs(readiness): say tests are declared, not passing

`cargo test -- --list` counts declared tests; an #[ignore] would keep
the count while "pass" became false. rust-ci is what runs them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4
---
 READINESS.adoc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/READINESS.adoc b/READINESS.adoc
index 7cd3c63..f81065c 100644
--- a/READINESS.adoc
+++ b/READINESS.adoc
@@ -8,7 +8,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 
 === CRG Grade: D (Alpha — Unstable)
 
-*Justification:* 119 tests pass (`cargo test --workspace --locked -- --list`); the
+*Justification:* 119 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
 Idris2 ABI does not typecheck, so 0 proofs are checked (#145); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips,
 benchmarks measured fake crypto until this session. RSR compliance
@@ -64,7 +64,7 @@ handling
 (requires idris2 binary)
 |===
 
-*Total passing:* 119 tests + 5 benchmark groups; 0 Idris2 proofs checked (#145) *Total
+*Total declared:* 119 tests + 5 benchmark groups; 0 Idris2 proofs checked (#145) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix