When Kani Exploration Stalls: Record the Boundary Before Narrowing It

When exploration gets smaller, what does the result establish?

A small Kani harness may finish quickly. Collections, loops and deep call graphs can make another harness exceed its time or memory budget.

Reducing eight inputs to four, adding kani::assume, or replacing an expensive function with a stub can make verification manageable. The essential practice is to keep the original claim connected to the claim supported by the eventual result.

This companion to Formal Verification in the Development Loop covers proof journals, assumption classification and outstanding verification obligations. Kani’s official guidance also describes isolating loops, symbolic types and expensive arithmetic, changing solvers and partitioning inputs. [1]

The example bundle contains a fictional state machine, harnesses, a journal, an assumption registry, empty run records and a standalone loop-contract example. Rust builds/tests, Kani/CBMC, coverage and timing/memory measurements were not executed. This is not a report that the small example was actually slow. Proposed work and observed evidence remain separate.

1. Separate claim, model, search conditions and outcome

“Kani verified it” does not identify what a reader can rely on. Keep at least these records alongside the code:

A run that does not finish establishes neither safety nor a bug by itself. Preserve which phase was reached: compilation, unwinding, solver execution or another stage. Identify the problem and conditions before generalizing that Kani is slow.

The real-code guide recommends avoiding many loops, complex data structures, I/O, deep call graphs and substantial global state as initial targets. Difficulty can suggest a responsibility worth separating, but it is not by itself proof of bad architecture. [2]

2. Define the transition and the history property

The example moves a job from Pending through Approved and Executing to Done or Failed. Unsupported commands leave the state unchanged; Done and Failed are terminal. These educational semantics differ from the previous article’s transition API returning Result.

#[derive(Copy, Clone, Debug, Eq, PartialEq)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum JobState { Pending, Approved, Executing, Done, Failed }

#[derive(Copy, Clone, Debug, Eq, PartialEq)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum Command { Approve, Start, Complete, Fail }

// This educational model treats unsupported transitions as no-ops.
// It is distinct from the earlier article's Result-returning transition API.
pub fn transition(state: JobState, command: Command) -> JobState {
    match (state, command) {
        (JobState::Pending, Command::Approve) => JobState::Approved,
        (JobState::Approved, Command::Start) => JobState::Executing,
        (JobState::Executing, Command::Complete) => JobState::Done,
        (JobState::Executing, Command::Fail) => JobState::Failed,
        _ => state,
    }
}

The property is: if execution starts in Pending and finishes in Done, it previously visited Executing. Update the history flag from the state before applying the command. Setting it merely because Done was reached would embed the desired conclusion into the instrumentation.

// History records the state BEFORE this command is applied.
// Entering Done does not itself set the history flag.
pub fn step_with_history(state: JobState, seen: bool, command: Command)
    -> (JobState, bool)
{
    (transition(state, command), seen || state == JobState::Executing)
}

pub fn run_with_trace(mut state: JobState, commands: &[Command]) -> (JobState, bool) {
    let mut seen = state == JobState::Executing;
    let mut index = 0;
    while index < commands.len() {
        (state, seen) = step_with_history(state, seen, commands[index]);
        index += 1;
    }
    (state, seen)
}

Review the trace code too. This flag observes in-process transitions; it is not evidence of durable audit-log completeness or that an external job actually ran. If the initial state changes to an arbitrary restored state, revisit initial Done and missing history before reusing the claim.

3. Exactly eight is different from zero through eight

Passing let commands: [Command; 8] = kani::any(); directly to the runner represents exactly eight commands. Labeling a registry field max_length: 8 does not explicitly include empty or shorter sequences.

Terminal-state and no-op semantics might support a separate padding argument for some properties. That argument should not remain implicit. Instead, model the length symbolically and represent zero through eight directly.

fn history_invariant(state: JobState, seen: bool) -> bool {
    state != JobState::Done || seen
}

/// JOB-001: all represented lengths from zero through eight.
/// Unwind 9 is a proposed setting, not an observed sufficient bound.
#[kani::proof]
#[kani::unwind(9)]
fn job_001_up_to_eight() {
    let storage: [Command; 8] = kani::any();
    let len: usize = kani::any();
    // V-001: verification-only size limit; no production batch contract exists.
    kani::assume(len <= storage.len());
    let (state, seen) = run_with_trace(JobState::Pending, &storage[..len]);
    kani::cover!(len == 0, "empty sequence is represented");
    kani::cover!(state == JobState::Done, "Done is reachable");
    kani::cover!(state == JobState::Failed, "Failed is reachable");
    assert!(history_invariant(state, seen));
}

The eight-element storage array is already a representation bound. Searching only for assume statements will miss such restrictions. This harness concerns every represented command sequence of length zero through eight. It does not cover arbitrary lengths, concurrency, persistence or distributed retries.

#[kani::unwind(9)] is a proposed setting for this simple loop, not an observed sufficient bound. Input bounds and unwinding have different meanings.

4. Use small unwinding to diagnose incomplete exploration

Kani’s guide suggests starting with #[kani::unwind(1)] to stop expansion early and isolate a problem. This does not guarantee quick termination: expensive work before a loop or elsewhere can still dominate. A process-wide time and memory budget is a separate control. [2][3]

# Proposed runs; not executed for this article.
cargo kani --harness job_001_up_to_eight --unwind 1
cargo kani --harness job_001_up_to_eight --unwind 4
cargo kani --harness job_001_up_to_eight --unwind 9

For a selected harness, --unwind can override its annotation. --default-unwind supplies a bound where one is not explicitly set. Source annotations alone therefore do not reconstruct the run: keep the complete command. [3][4]

An unwinding assertion failure indicates that the chosen expansion did not account for loop completion. A successful target assertion alongside unresolved or UNDETERMINED checks is not completion of the required proof. Disabling the unwinding check does not resolve the missing exploration.

The tutorial describes a simple loop needing a bound one greater than its iterations, and more complex relationships with break, continue and related control flow. Treat nine for eight iterations as a candidate, not a universal rule. Inspect the loop structure and actual checks. [3]

Not every performance improvement narrows a guarantee. Incomplete exploration also cannot simply be relabeled a successful smaller proof.

5. Classify each assumption by its reason

kani::assume(condition) excludes paths that do not satisfy the condition; it is not a search-order hint. The FAQ explains that checks after assume(false) become UNREACHABLE. [5]

This addition clearly reduces the example’s scope:

// V-002: verification-only reduction; see verification/JOB-001.md.
kani::assume(len <= 4);

The bundle preserves the original harness and supplies job_001_reduced_to_four separately. There is no measured claim that four is faster. Keep both the comparison candidate and the original zero-through-eight obligation.

If production really rejects batches above MAX_BATCH=32, that bound can be a legitimate precondition. Establish it at every relevant entry point, including batch execution, internal callers and restored data. A harness assumption does not implement runtime validation.

Introducing a product limit requires a decision involving requirements, latency and operational clarity. Do not silently promote a verification convenience of four inputs into a business requirement.

6. Use covers to investigate vacuous success

The implication “Done implies seen” has no counterexample if Done cannot be reached. Two commands from Pending cannot complete Approve → Start → Complete. In this model, the Done cover is expected to be unreachable by inspection; no Kani result has been collected.

The standalone diagnostic_two_command_vacuity harness investigates that distinction. Keep intentionally unreachable covers outside an undifferentiated all-green verification gate.

A satisfied cover! supplies existential evidence: some modeled execution reaches that condition. An assertion checks a property across the modeled executions. Retain their outcomes separately. Covers for Done and Failed do not establish that every business scenario or input combination is represented. [5]

Source coverage provides another diagnostic. In the referenced version it is experimental. [6]

cargo kani \
  --coverage -Z source-coverage \
  --harness job_001_up_to_eight \
  --unwind 9

For a NONE line, ask whether the domain legitimately excludes it or an added assumption removed it. Conversely, FULL on every line is not full path or requirement coverage. Property/harness review and separately planned mutation checks can investigate whether a specific defect would actually be detected.

7. Distinguish decomposition from replacing a function

If authorization verification reaches a database, parser, network client and cache, consider extracting the pure policy decision. Kani’s real-code guide recommends separating I/O from pure computation rather than expecting direct verification of external I/O behavior. [2]

One claim might say that a valid principal, policy and action never yield an unauthorized Allow. Another checks that adapters load and translate external state correctly. Kani can address the first; integration evidence can address the second. A correct core still makes the wrong system decision if an adapter supplies an old policy or the wrong user. Record that correspondence obligation.

Stubbing is a different operation. #[kani::stub(original, replacement)] replaces a function with another implementation. The reference describes experimental -Z stubbing; an ordinary replacement is not automatically proved equivalent to the original. [7]

Replacing a parser with “any valid policy” may broadly cover successful values while removing parse-error paths. It can also lose relationships between inputs and outputs or side effects. An overapproximation may preserve a safety claim; an underapproximation may hide real failures. Justify the inclusion relation and the kind of property before transferring the result to the original implementation.

8. Preserve claims through contracts and input partitions

Kani function contracts use requires and ensures, proof_for_contract for callee obligations, and stub_verified for caller-side abstraction. The referenced interface uses -Z function-contracts. [8]

The word “verified” in an attribute is not a substitute for corresponding execution evidence. Link contract and callee revisions, preconditions, return guarantees, modified state and caller-side precondition establishment. A property absent from the contract is not automatically available to the caller.

Input partitioning is another approach. Prove the same property separately for lengths 0–4 and 5–8, then justify that their union covers 0–8. Completion of the first partition alone does not close the original obligation. Review gaps, off-by-one boundaries and differing stub assumptions across partitions. [1]

The state machine offers another decomposition. Define I(state, seen) = state != Done || seen, and separate the base case from one-step preservation.

/// Separate induction obligations; see the journal's composition limits.
#[kani::proof]
fn job_001_induction_base() {
    assert!(history_invariant(JobState::Pending, false));
}

#[kani::proof]
fn job_001_induction_step() {
    let state: JobState = kani::any();
    let seen: bool = kani::any();
    let command: Command = kani::any();
    // IH-001: induction hypothesis, not a claim about arbitrary initial state.
    kani::assume(history_invariant(state, seen));
    let (next, next_seen) = step_with_history(state, seen, command);
    assert!(history_invariant(next, next_seen));
}

If both obligations are actually verified and the meaning of history and its correspondence to transitions are justified, ordinary mathematical induction can support the abstract transition relation over every finite trace. Both harnesses are currently unexecuted.

That argument alone does not verify allocation, indexing or termination of a concrete Rust wrapper on arbitrarily sized slices, or a real job scheduler. Retain the inductive transition claim and the bounded wrapper harness as separate obligations.

9. Treat loop contracts as a different proof method

Instead of unrolling every iteration, a loop contract abstracts the loop through an invariant. Kani’s experimental interface checks establishment, preservation and the postcondition implied at exit. It does not remove all input-representation or machine-type limits. [9]

For this example, processed <= commands.len() alone does not imply the history property. The invariant must also relate state and history, with a justified treatment of modified memory.

The following countdown is independent of JOB-001. It separates an invariant trivial for the type from a decreases expression describing progress. It is supplied as a standalone file, not part of the Cargo library.

// Standalone experimental example, NOT part of the Cargo library.
// Pin the Kani/Rust versions and enable -Z loop-contracts before future use.
#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

#[kani::proof]
fn countdown_contract() {
    let mut remaining: u8 = kani::any();
    #[kani::loop_invariant(remaining <= u8::MAX)]
    #[kani::loop_decreases(remaining)]
    while remaining > 0 {
        remaining -= 1;
    }
    assert_eq!(remaining, 0);
}

# Not run. Review feature/compiler requirements in the selected version.
kani experimental/countdown.rs -Z loop-contracts

An invariant alone does not establish termination. Distinguish partial correctness, describing the result if the loop terminates, from total correctness, which also establishes termination. An assertion after a loop having no counterexample is not automatically a progress guarantee.

The pinned documentation notes that side-effect-free contracts are not automatically enforced. It also describes loop_modifies inference, unsupported forms such as while let, and known decreases limitations involving struct fields, multiple measures, modifies combinations and nested loops. Review the selected version and keep contract expressions free of side effects. [9]

10. Do not collapse timeouts and counterexamples into one failure

A journal can classify outcomes per claim while retaining the tool’s raw output:

These are proposed journal labels, not a claim that Kani prints those exact words. An unwinding failure alone does not refute the business property. If a target assertion has a counterexample, examine its assumptions and stubs. A spurious abstraction trace differs from a counterexample to the real system. Do not classify a run from exit code or one success line alone.

The referenced Rust feature-support guide excludes concurrency and describes compiling concurrent code as sequential. Such a harness does not establish freedom from data races or cover all interleavings. Record unsupported boundaries such as inline assembly even when stubbing makes them disappear from a particular analysis. [10]

Execution records need the complete command, source revision and uncommitted patch hash, dependencies, Kani and its bundled Rust/CBMC, target, solver, flags, host/container limits, exit reason and raw logs. The documentation revision is distinct from the binary actually executed, especially for changing coverage and contract features.

11. Manage proof budgets and verification debt

Budgets such as 30 seconds locally, five minutes for a PR and 30 minutes nightly can be useful policies. They are examples, not measured timings for this harness. An enforced timeout must terminate and reap child processes and preserve partial logs, signals and timestamps. The bundle does not implement that runner.

GNU/Linux /usr/bin/time -v and macOS /usr/bin/time -l differ. Peak RSS can refer to a parent, a maximum involving children or another accounting scope; none automatically equals the simultaneous total of a process tree. Document the measurement and do not add unrelated maxima as an actual peak.

If one claim changes from 12 seconds to four minutes, compare toolchain, solver, host contention and cache conditions as well as source. A new loop or deeper call graph can provide design feedback. Do not narrow semantics merely because of one slow observation.

The supplied registry is NOT_RUN; revision, log, time and memory fields are null. Do not invent a timeout or a PROVED result before execution. The journal retains exact-eight, zero-through-eight, zero-through-four, diagnostic unwinding and induction candidates as separate records.

{
  "claim": "JOB-001",
  "result": {
    "status": "NOT_RUN",
    "reason": null,
    "source_revision": null,
    "source_patch_sha256": null,
    "toolchain": null,
    "raw_log": null,
    "wall_seconds": null,
    "peak_memory_bytes": null
  },
  "debt": {
    "id": "VD-001",
    "owner": null,
    "review_date": null,
    "remaining": "bounded_to_all_finite_trace_argument_and_execution"
  }
}

VD-001 tracks the distance between bounded zero-through-eight and all finite traces. A successful four-command result would not close it. Assign an owner and review date before operational adoption; missing values should not be filled with invented responsibility.

12. Review the guarantee diff alongside the result

A harness is specification code. Adding assume(action != Delete) removes evidence for a claim that includes Delete. Replacing kani::any() with a concrete value is useful diagnosis but also changes the model. Do not leave the diagnostic model behind under the original claim’s label.

Connect these items during review:

• Old and new claims and input domains, including empty inputs and initial states.
• Representation bounds, unwinding, assumptions, stubs/contracts and disabled checks.
• Required assertions and safety checks, cover witnesses and unresolved obligations.
• Execution artifacts tied to source, toolchain, flags and budgets.
• Partition completeness and outstanding verification debt.

The related authentication and authorization PoC supplies attributed design context. This article’s job model, harnesses, versions, coverage and performance are not claimed as evidence executed in that engagement. Tamarin implementation correspondence addresses another form of distance between a model and its system.

Smaller proofs can narrow a claim, partition the same claim, or provide an incomplete diagnostic. Name and record which operation occurred. The useful engineering result is not just a saved success message: it is being able to explain what succeeded, under which conditions, and what remains unresolved.

References

1. Debugging Slow Proofs — Slow-proof causes, solver selection and input partitioning.
2. Using Kani on Real Code — Target selection, I/O and small unwind bounds.
3. Loop Unwinding — Incomplete unwinding, checks and input bounds.
4. Using Kani — Harness selection and configuration.
5. Frequently Asked Questions — assume(false), unreachable checks and covers.
6. Source Coverage — Experimental line coverage.
7. Stubbing — Replacement semantics and experimental flags.
8. Function Contracts — Pre/postconditions, callee obligations and caller abstraction.
9. Loop Contracts — Invariants, decreases, side effects and known limitations.
10. Rust Feature Support — Concurrency, assembly and other support boundaries.

The documentation baseline is commit 103dca2dfae56ad9a0dd48df83c0a4f84583abe3. This identifies a documentation baseline, not a claim that the example ran with a binary built from that commit.