leynos · leynos · Aug 2, 2026 · Jul 28, 2026 · Jul 28, 2026 · Aug 1, 2026
diff --git a/.cargo/config.toml b/.cargo/config.toml
@@ -1,10 +1,12 @@
 # Enable the Polonius alpha borrow-checking analysis for every Cargo
-# invocation, including rust-analyzer and `cargo kani`, so editors and
-# verification tooling agree with CI about what borrows are legal.
+# invocation, including rust-analyzer, so editors and verification tooling
+# agree with CI about what borrows are legal.
 #
 # Note: an inherited `RUSTFLAGS` environment variable overrides this table.
 # Wrappers that set `RUSTFLAGS` (see the Makefile) must re-state
-# `-Zpolonius=next` themselves. See
+# `-Zpolonius=next` themselves. `cargo kani` sets `CARGO_ENCODED_RUSTFLAGS`
+# itself, which also bypasses this table, so the `kani-full` recipe passes
+# the flag via `RUSTFLAGS`. See
 # docs/adr-006-adopt-polonius-nightly-toolchain.md.
 [build]
 rustflags = ["-Zpolonius=next"]
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -112,6 +112,7 @@ jobs:
   kani-smoke:
     if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     permissions:
       contents: read
     env:
@@ -140,3 +141,5 @@ jobs:
         run: make install-kani
       - name: Kani version check
         run: make kani-check
+      - name: Run Kani harnesses
+        run: make kani-ir
diff --git a/Makefile b/Makefile
@@ -80,10 +80,10 @@ clean: ## Remove build artefacts
 test: test-nextest doctest ## Run every Rust test with warnings treated as errors
 
 test-nextest: ## Run all non-doctest Rust tests through cargo-nextest
-	RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) nextest run --all-targets --all-features $(NEXTEST_BUILD_JOBS)
+	RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) nextest run --all-targets --all-features $(NEXTEST_BUILD_JOBS)
 
 doctest: ## Run doctests, which cargo-nextest cannot execute
-	RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) test --doc --all-features $(BUILD_JOBS)
+	RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) test --doc --all-features $(BUILD_JOBS)
 
 test-workflow-contracts: ## Validate the mutation-testing caller contract
 	uv run --with 'pytest>=8' --with 'pyyaml>=6' pytest tests/workflow_contracts -q
@@ -97,10 +97,10 @@ lint: lint-clippy lint-whitaker ## Run Clippy and the Whitaker Dylint suite with
 
 lint-clippy: ## Run rustdoc and Clippy with warnings denied
 	RUSTDOCFLAGS="$(RUSTDOC_FLAGS)" RUSTFLAGS="$${RUSTFLAGS-} $(POLONIUS_FLAGS)" $(CARGO) doc --no-deps
-	RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) clippy $(CLIPPY_FLAGS)
+	RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) clippy $(CLIPPY_FLAGS)
 
 lint-whitaker: ## Run the Whitaker Dylint suite with warnings denied
-	RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(WHITAKER) --all -- --all-targets --all-features
+	RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(WHITAKER) --all -- --all-targets --all-features
 
 fmt: ## Format Rust and Markdown sources
 	$(CARGO) fmt --all
@@ -110,7 +110,7 @@ check-fmt: ## Verify formatting
 	$(CARGO) fmt --all -- --check
 
 typecheck: ## Typecheck all targets and features
-	RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) check --all-targets --all-features $(BUILD_JOBS)
+	RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) check --all-targets --all-features $(BUILD_JOBS)
 
 markdownlint: spelling ## Lint Markdown and enforce en-GB-oxendict spelling
 	$(MDLINT) "**/*.md"
@@ -146,7 +146,7 @@ kani-check: ## Check the installed Kani verifier version
 	@$(PROVER_TOOLS) kani check-version --kani-command "$(KANI)" $(KANI_CHECK_FLAGS) || { status=$$?; printf 'prover-tools: target=kani-check failed exit=%s\n' "$$status" >&2; exit "$$status"; }
 
 kani-full: ## Run the full Kani verification suite
-	$(KANI) $(KANI_FLAGS)
+	RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }$(POLONIUS_FLAGS)" $(KANI) $(KANI_FLAGS)
 
 kani-ir: kani-full ## Run the IR Kani verification suite
 

diff --git a/docs/adr-006-adopt-polonius-nightly-toolchain.md b/docs/adr-006-adopt-polonius-nightly-toolchain.md
@@ -1,4 +1,4 @@
-# Architecture Decision Record (ADR): Adopt the Polonius borrow checker on a pinned nightly toolchain
+# Architecture decision record (ADR): Adopt the Polonius borrow checker on a pinned nightly toolchain
 
 ## Status
 
@@ -39,9 +39,12 @@ Adopt Polonius now, as a nightly-only source tree:
 - Pin the dated toolchain `nightly-2026-06-25` in `rust-toolchain.toml` so
   builds stay reproducible.
 - Enable `-Zpolonius=next` in `.cargo/config.toml` under `[build] rustflags`,
-  so plain Cargo invocations, rust-analyzer, and `cargo kani` all borrow-check
-  with the same analysis. Makefile recipes that set `RUSTFLAGS` (which
-  overrides that table) re-state the flag via the `POLONIUS_FLAGS` variable.
+  so plain Cargo invocations and rust-analyzer borrow-check with the same
+  analysis. Makefile recipes that set `RUSTFLAGS` (which overrides that table)
+  re-state the flag via the `POLONIUS_FLAGS` variable. `cargo kani` sets
+  `CARGO_ENCODED_RUSTFLAGS` itself, which also bypasses the table, so the
+  `kani-full` recipe passes the flag through the `RUSTFLAGS` environment
+  variable, which Kani appends to its own flags.
 - Collapse the CI matrices in `ci.yml` and `netsukefile-test.yml` to the
   pinned nightly, and align `coverage-main.yml`. Stable and MSRV legs are
   removed because the tree no longer compiles without Polonius.

diff --git a/docs/developers-guide.md b/docs/developers-guide.md
@@ -82,10 +82,16 @@ Netsuke builds on the dated nightly toolchain pinned in `rust-toolchain.toml`
 with the Polonius alpha borrow-checking analysis (`-Zpolonius=next`) enabled.
 `rustup` provisions the toolchain automatically, and `.cargo/config.toml`
 supplies the flag by default, covering Cargo invocations such as rust-analyzer
-and `cargo kani` that run without `RUSTFLAGS` in the environment. Makefile
-recipes that set `RUSTFLAGS` re-state the flag through the `POLONIUS_FLAGS`
-variable because an inherited `RUSTFLAGS` environment variable overrides
-`.cargo/config.toml`.
+that run without `RUSTFLAGS` in the environment. Makefile recipes that set
+`RUSTFLAGS` re-state the flag through the `POLONIUS_FLAGS` variable because an
+inherited `RUSTFLAGS` environment variable overrides `.cargo/config.toml`. The
+recipes that add `-D warnings` and `$(POLONIUS_FLAGS)` build the value as
+`RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)"`; the
+`$${RUSTFLAGS:+$$RUSTFLAGS }` expansion prepends any `RUSTFLAGS` already set by
+the caller (for example a CI wrapper), so those flags survive rather than being
+silently discarded. `cargo kani` sets `CARGO_ENCODED_RUSTFLAGS` itself, which
+also overrides the table, so `make kani-full` passes the flag through
+`RUSTFLAGS` as well.
 
 [ADR-006](adr-006-adopt-polonius-nightly-toolchain.md) records the policy
 decision, and the [polonius migration notes](polonius.md) track every site
@@ -845,10 +851,12 @@ for the design rationale and re-entry criteria.
 
 Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary
 `build-test` job. The job installs `uv`, installs the pinned Kani version
-through `make install-kani`, and runs only `make kani-check`; it does not run
-`make kani-full`, `make verus`, coverage, CodeScene upload, or the normal build
-matrix. Its cache is intentionally separate from ordinary Cargo build
-artefacts: the job uses a Kani-specific cache key derived from
+through `make install-kani`, runs `make kani-check` as a version-drift guard,
+and then runs the bounded harness suite through `make kani-ir` under a
+20-minute job timeout; it does not run `make verus`, coverage, CodeScene
+upload, or the normal build matrix. Its cache is intentionally separate from
+ordinary Cargo build artefacts: the job uses a Kani-specific cache key derived
+from
 `tools/kani/VERSION` and the Makefile, then caches the job-local Kani Cargo
 home plus Kani support-file home.
 
@@ -858,9 +866,11 @@ home plus Kani support-file home.
 
 - `make test-nextest` —
   `cargo nextest run --all-targets --all-features`, with
-  `RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)"` (the Makefile re-states the
-  Polonius flag because a set `RUSTFLAGS` overrides `.cargo/config.toml`). This
-  runs every unit, integration, `rstest`, and `rstest-bdd` test.
+  `RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)"` (the
+  Makefile re-states the Polonius flag because a set `RUSTFLAGS` overrides
+  `.cargo/config.toml`, and the `$${RUSTFLAGS:+$$RUSTFLAGS }` prefix preserves
+  any `RUSTFLAGS` inherited from the caller). This runs every unit,
+  integration, `rstest`, and `rstest-bdd` test.
 - `make doctest` — `cargo test --doc --all-features`, with the same
   `RUSTFLAGS`. nextest cannot execute doctests, so they need their own pass.
   Note that the previous `cargo test --all-targets` invocation never ran

diff --git a/docs/execplans/4-1-2-kani-smoke-ci-job.md b/docs/execplans/4-1-2-kani-smoke-ci-job.md
@@ -569,3 +569,19 @@ The references section should include:
 - Lody session:
   <https://lody.ai/leynos/sessions/48bbbaef-5f08-49d0-9666-fa4506326e10>
 ```
+
+## Addendum: 2026-08-02 — bounded harness wiring completed
+
+The bounded Kani harness work deferred at the time of this ExecPlan's
+execution has since been completed, in follow-up work tracked as
+[issue #445](https://github.com/leynos/netsuke/issues/445). The pull-request
+`kani-smoke` job now runs `make kani-check` (the pinned-version drift guard)
+and then `make kani-ir` (the bounded harness suite), after
+`make install-kani`. The `kani-smoke` job declares `timeout-minutes: 20`. The
+bounded suite contains 13 `#[kani::proof]` harnesses: 4 in
+`src/ir/from_manifest_verification.rs` and 9 in
+`src/ir/cycle_verification.rs`.
+[Pull request #470](https://github.com/leynos/netsuke/pull/470) carries the
+implementation and declares `Closes #445`; the issue itself remains open at
+the time of writing and closes on merge. This addendum records later work and
+does not amend the plan as executed.
diff --git a/docs/formal-verification-methods-in-netsuke.md b/docs/formal-verification-methods-in-netsuke.md
@@ -216,8 +216,10 @@ development and continuous integration. These pins serve several purposes:
 The first formal-verification commands should extend the existing `Makefile`
 without disturbing the current developer workflow.[^2]
 
-- `make kani-check` should run the fast installed-version check suitable for
-  pull requests until substantive Kani harnesses exist.
+- `make kani-check` should run the fast pinned-version drift guard suitable
+  for pull requests.
+- The bounded Kani harness suite now also runs on pull requests through
+  `make kani-ir`.
 - `make kani-full` should run the full Kani suite.
 - `make install-kani` should install the pinned Kani version through
   `rust-prover-tools`.
@@ -236,12 +238,16 @@ Formal verification should not be folded into the existing `build-test` job.
 The current `CI` workflow already performs formatting, linting, tests, and
 coverage, and those checks should remain intact.[^3]
 
-The first additional job should be a dedicated `kani-smoke` job that:
+The `kani-smoke` job is a dedicated, pull-request-only job (it runs only when
+`github.event_name == 'pull_request'`) that:
 
 - installs `uv` and then installs the pinned Kani toolchain through
   `make install-kani`,
-- runs `make kani-check`, and
-- caches tool downloads separately from the ordinary Rust build artefacts.
+- runs `make kani-check` and then the bounded harness suite through
+  `make kani-ir` (13 harnesses across the manifest-verification and
+  cycle-verification modules),
+- caches tool downloads separately from the ordinary Rust build artefacts, and
+- is bounded by a 20-minute job timeout (`timeout-minutes: 20`).
 
 Any later Verus job should be added only after a stable proof kernel exists.
 

diff --git a/docs/roadmap.md b/docs/roadmap.md
@@ -355,11 +355,10 @@ and test workflow intact. See
   Requires 4.1.1. See
   [formal-verification-methods-in-netsuke.md §Continuous integration (CI)](formal-verification-methods-in-netsuke.md#continuous-integration-ci).
   - [x] Keep the existing `build-test` job unchanged.
-  - [x] Run the bounded smoke path on pull requests. As scoped for this item,
-    the `kani-smoke` job in `.github/workflows/ci.yml` runs `make install-kani`
-    and `make kani-check` (a Kani version check); the harness set was empty when
-    this lane shipped. Wiring the bounded harnesses since landed by `4.2.*` into
-    the pull-request job is tracked separately as
+  - [x] Run the bounded smoke path on pull requests. The `kani-smoke` job in
+    `.github/workflows/ci.yml` runs `make install-kani`, `make kani-check` (a
+    Kani version check), and `make kani-ir` (the bounded harnesses landed by
+    `4.2.*`). The harness wiring resolved the follow-up previously tracked as
     [issue #445](https://github.com/leynos/netsuke/issues/445).
   - [x] Cache Kani tool downloads separately from ordinary Cargo artefacts.
 - [x] 4.1.3. Record the phase-1 scope boundary for Verus and Stateright. See

diff --git a/src/ir/cycle.rs b/src/ir/cycle.rs
@@ -28,7 +28,9 @@ mod cycle_property_tests;
 mod support;
 #[cfg(any(test, kani))]
 use support::canonicalize_cycle_by;
-use support::{canonicalize_cycle, path_cmp, path_eq, state_for_path, target_entry_for_path};
+#[cfg(not(kani))]
+use support::path_cmp;
+use support::{canonicalize_cycle, path_eq, state_for_path, target_entry_for_path};
 
 #[cfg(test)]
 #[path = "cycle_tests.rs"]

diff --git a/src/ir/cycle_verification.rs b/src/ir/cycle_verification.rs
@@ -1,5 +1,6 @@
 //! Kani harnesses for bounded IR cycle-handling properties.
 
+use super::support::rotate_index;
 use super::*;
 
 /// Prove a self-dependency reports a cycle and no missing dependency.