fix: gate WASM CLI-spec registration on unix; fix all-features test compile; monotonic RPC rate limiter

.github/workflows/ci.yml

@@ -1073,11 +1073,46 @@ jobs:
           mkdir -p "${RUNNER_TEMP}/cargo"
           echo "CARGO_HOME=${RUNNER_TEMP}/cargo" >> "$GITHUB_ENV"
 
+      # Build runs last on a host that test/clippy/docs/fuzz may already have filled.
+      # Free space before restoring the target cache, and skip that restore when
+      # space is still short (run 39430830510 hit ENOSPC during restore + unpack).
+      - name: Low-disk guard before cache restore
+        id: disk
+        run: |
+          df -h / "${{ github.workspace }}" /mnt/data 2>/dev/null || true
+          CARGO_TEMP="${RUNNER_TEMP}/cargo"
+          if [ -d "$CARGO_TEMP" ]; then
+            rm -rf "$CARGO_TEMP/registry/src" "$CARGO_TEMP/git/checkouts" 2>/dev/null || true
+          fi
+          BUILD_ROOT="${BLVM_RUNNER_DATA_ROOT}"
+          RUN_ID="${{ github.run_id }}"
+          if [ -d "$BUILD_ROOT" ]; then
+            find "$BUILD_ROOT" -mindepth 1 -maxdepth 1 -type d \
+              -not -name "$RUN_ID" \
+              -exec rm -rf {} + 2>/dev/null || true
+          fi
+          rm -rf fuzz/target 2>/dev/null || true
+          AVAIL=$(df -B1 "${{ github.workspace }}" | tail -1 | awk '{print $4}')
+          MIN_FREE=$((20 * 1024 * 1024 * 1024))
+          if [ -n "$AVAIL" ] && [ "$AVAIL" -lt "$MIN_FREE" ]; then
+            echo "::warning::Only $AVAIL bytes free; skipping target cache restore (cold build)"
+            echo "restore-target=false" >> "$GITHUB_OUTPUT"
+          else
+            echo "restore-target=true" >> "$GITHUB_OUTPUT"
+          fi
+          df -h "${{ github.workspace }}" || true
+
+      - name: Prune runner caches
+        uses: BTCDecoded/rust-ci/runner-cargo-cache@main
+        with:
+          operation: prune
+
       - name: Cache
         uses: BTCDecoded/rust-ci/runner-cargo-cache@main
         with:
           operation: bind-env
           cache-key: ${{ needs.setup.outputs.cache-key }}
+          include-target: ${{ steps.disk.outputs.restore-target }}
 
       - name: Restore Cargo cache
         uses: BTCDecoded/rust-ci/runner-cargo-cache@main

Cargo.toml

@@ -330,6 +330,8 @@ criterion = "=0.5.1"
 proptest = "=1.5.0"
 dhat = "=0.3"  # Heap profiling
 serial_test = "=3.0"  # Sequential test execution for database isolation
+# Paused/advanced tokio clock for deterministic rate-limiter tests (same version as the main dep)
+tokio = { version = "=1.48.0", features = ["test-util"] }
 
 # Release profile optimizations (mirrors blvm-consensus)
 [profile.release]

SECURITY.md

@@ -172,7 +172,7 @@ This document defines the security boundaries, threat model, and limitations of
 
 #### Phase 3: Mainnet Hardening
 - [ ] Professional security audit (external, requires security firm)
-- [x] Formal verification of critical paths (property tests for node invariants added)
+- [x] Property tests for node invariants on critical paths (testing, not formal verification)
 - [x] Advanced peer management (connection quality tracking, peer selection, reliability scoring)
 - [x] Performance optimization (performance profiler infrastructure added)
 - [x] Monitoring and alerting (metrics collection, health checks, RPC endpoints)

docs/NETWORK_VERIFICATION.md

@@ -1,14 +1,14 @@
-# Network Protocol Formal Verification
+# Network Protocol Spec-Lock Checks
 
 ## Overview
 
-This document describes formal verification of Bitcoin P2P protocol message parsing, serialization, and processing. Verification uses **blvm-spec-lock** (Z3-based) for consensus code and Dandelion (Section 10.6).
+This document describes the spec-lock checks on Bitcoin P2P protocol message parsing, serialization, and processing. Functions are annotated with `#[spec_locked]` and Z3-checked by **blvm-spec-lock** (consensus code and Dandelion, Section 10.6). An annotated, Z3-checked function is not formally verified: in blvm-consensus only 3 of 182 anchors are mutation-validated (see [`docs/VERIFICATION.md`](https://github.com/BTCDecoded/blvm-consensus/blob/main/docs/VERIFICATION.md)).
 
 ## Verification Status
 
 ### blvm-spec-lock (Orange Paper)
 
-- **Dandelion (10.6)** – ✅ Verified in `src/network/dandelion.rs` via `#[spec_locked("10.6")]`
+- **Dandelion (10.6)** – annotated and Z3-checked in `src/network/dandelion.rs` via `#[spec_locked("10.6")]`
 - **Protocol parsing (10.1)** – ✅ Covered: parse_message, calculate_checksum (protocol-verification feature, enabled by default)
 
 ### Planned spec-lock coverage
@@ -35,7 +35,7 @@ cargo spec-lock verify --crate-path . \
 
 ### CI
 
-Formal verification runs via **blvm-spec-lock** in **`.github/workflows/ci.yml`** (**verify** job): installs **`cargo-spec-lock`** from crates.io, runs **`verify`** on the published **blvm-consensus** sources and again on **blvm-node** (merged **`F_*`** gate + Rust rows; **`formula_registry`** in **`spec_lock_*_verify.json`**). Report shape and **`jq`**: **`blvm-spec-lock`** **`docs/VERIFY_JSON.md`**.
+Spec-lock checks run via **blvm-spec-lock** in **`.github/workflows/ci.yml`** (**verify** job): installs **`cargo-spec-lock`** from crates.io, runs **`verify`** on the published **blvm-consensus** sources and again on **blvm-node** (merged **`F_*`** gate + Rust rows; **`formula_registry`** in **`spec_lock_*_verify.json`**). Report shape and **`jq`**: **`blvm-spec-lock`** **`docs/VERIFY_JSON.md`**.
 
 ## References
 

src/module/traits.rs

@@ -492,7 +492,7 @@ pub trait NodeAPI: Send + Sync {
     /// Get block template (GBT equivalent)
     ///
     /// Returns a block template suitable for mining.
-    /// Uses the same formally verified consensus function as RPC getblocktemplate.
+    /// Uses the same tested blvm-consensus mining function as RPC getblocktemplate.
     ///
     /// # Arguments
     /// * `rules` - Consensus rules to apply (e.g., ["segwit"])