chore: Shan-readiness — docs/AGENTS/.bazelversion + Verus quickstart doc

.bazelversion

@@ -0,0 +1 @@
+9.1.0

AGENTS.md

@@ -106,20 +106,29 @@ Key rules:
 
 ### Running verification locally
 
+The Bazel rules pull `nix-build` themselves for toolchain resolution
+(see `rules_rocq_rust` in MODULE.bazel) — `nix-build` must be on PATH,
+but `nix develop` and a flake.nix are NOT required. Just plain Bazel:
+
 ```bash
-# Verus SMT (requires Nix)
-nix develop --command bazel test //:verus_test
+# Verus SMT
+bazel test //:verus_test
 
 # Kani BMC
-nix develop --command bazel test //:kani_test //:kani_ffi_test
+bazel test //:kani_test //:kani_ffi_test
 
 # Rocq proofs
-nix develop --command bazel test //proofs:all
+bazel test //proofs:all
 
 # Lean proofs
-nix develop --command bazel test //proofs/lean:all
+bazel test //proofs/lean:all
 ```
 
+If your `bazel test` run fails with `nix-build not found in PATH`,
+prepend Nix's profile bin dir (typical install paths are
+`/nix/var/nix/profiles/default/bin` or `~/.nix-profile/bin`) to PATH
+and rerun.
+
 ## Conventions
 
 - Artifact IDs follow the pattern: PREFIX-NNN (e.g., REQ-001, FEAT-042)

README.md

@@ -18,7 +18,15 @@ Part of the [PulseEngine](https://github.com/pulseengine) toolchain.
 
 ## Modules
 
-39 Rust modules covering the full Zephyr kernel surface. All 39 pass Verus SMT verification (805 verified, 0 errors):
+39 Rust modules covering the full Zephyr kernel surface. All 39 pass Verus SMT verification (805 verified, 0 errors)¹:
+
+¹ "Verified" here = the bodies Verus checked against requires/ensures
+contracts. Trusted-base inventory (133 `#[verifier::external_body]`
+shims + 2 `assume_specification` calls): see
+[docs/safety/verification-honesty.md](docs/safety/verification-honesty.md).
+The headline number is anchored by the `formal-verification.yml` CI job
+(`bazel test //:verus_test`); if that job is red, the number is stale
+until it goes green again.
 
 **Synchronization**