Kani Harnesses

Kani is a bounded model checker for Rust, built on CBMC. Chio ships fourteen public harnesses against chio-kernel-core and runs the full sweep on every PR. The harnesses live in crates/chio-kernel-core/src/kani_public_harnesses.rs and crates/chio-kernel-core/src/kani_harnesses.rs.

What Kani Does

Kani translates a Rust function annotated with #[kani::proof] into a symbolic-execution problem and hands it to CBMC. CBMC searches all reachable executions for assertion failures, panics, and undefined behavior up to the configured bounds.

A typical harness looks like this:

#[kani::proof]
fn budget_commit_never_increases_remaining_counters() {
    let remaining_invocations = u64::from(kani::any::<u8>());
    let remaining_units = u64::from(kani::any::<u8>());
    let invocation_cost = u64::from(kani::any::<u8>());
    let unit_cost = u64::from(kani::any::<u8>());

    let committed = budget_commit(
        remaining_invocations,
        remaining_units,
        invocation_cost,
        unit_cost,
    );

    assert!(committed.remaining_invocations <= remaining_invocations);
    assert!(committed.remaining_units <= remaining_units);
}

kani::any::<u8>() introduces a symbolic byte; the u64::from widening keeps the symbolic state space small (256 distinct values per slot) while still exercising every branch of budget_commit. The two assertions are the property: a successful commit cannot increase either remaining counter.

Public Harnesses

Source: crates/chio-kernel-core/src/kani_public_harnesses.rs. These target the public API of chio-kernel-core: verify_capability, NormalizedScope::is_subset_of, scope::resolve_matching_grants, evaluate, and receipts::sign_receipt.

Every harness uses the lane-wide bound --default-unwind 8 --no-unwinding-checks from scripts/check-kani-public-core.sh. Wall-clock budgets come from the [lanes.pr] measurement block in formal/rust-verification/kani-public-harnesses.toml:47-62 (kani 0.67.0 on aarch64-apple-darwin, hot cargo cache).

Worked example: verify_revocation_predicate_idempotent

Quoted verbatim from kani_public_harnesses.rs:406-424:

#[kani::proof]
fn verify_revocation_predicate_idempotent() {
    let token_revoked = kani::any::<bool>();
    let ancestor_revoked = kani::any::<bool>();

    let first = revocation_snapshot_denies(token_revoked, ancestor_revoked);
    let second = revocation_snapshot_denies(token_revoked, ancestor_revoked);

    // Idempotence in the no-side-effects sense: re-evaluating the predicate on
    // the same revocation snapshot returns the same boolean.
    assert_eq!(first, second);

    // Boolean idempotence of `||` also forces `denies(x, x) == denies(x, x)`
    // independent of which leg fires. Pin both interpretations.
    let mirrored_first = revocation_snapshot_denies(token_revoked, token_revoked);
    let mirrored_second = revocation_snapshot_denies(token_revoked, token_revoked);
    assert_eq!(mirrored_first, mirrored_second);
    assert_eq!(mirrored_first, token_revoked);
}

Two free booleans give a four-element symbolic state space: (false, false), (false, true), (true, false), (true, true). CBMC unfolds each branch of revocation_snapshot_denies and discharges the three assertions on every assignment. The first assertion pins referential transparency: calling the predicate twice with the same snapshot returns the same boolean (no hidden state). The mirrored pair pins the diagonal collapse: when the revoked set is the union of the token and its ancestors and both coincide, the predicate reduces to a single revocation flag. That diagonal is what the TLA+ NoAllowAfterRevoke invariant relies on at refinement time.

CI lane split

From formal/rust-verification/kani-public-harnesses.toml:71-92:

[lanes.pr]
description = "Fast Kani harnesses run on every pull request (full sweep)"
harnesses = [
  "public_verify_capability_rejects_untrusted_issuer_before_signature",
  "public_normalized_scope_subset_rejects_widened_child",
  "public_normalized_scope_subset_rejects_value_widened_child",
  "public_normalized_scope_subset_rejects_identity_mismatch",
  "public_resolve_matching_grants_rejects_out_of_scope_request",
  "public_resolve_matching_grants_preserves_wildcard_matching",
  "public_evaluate_rejects_untrusted_issuer_before_dispatch",
  "public_sign_receipt_rejects_kernel_key_mismatch_before_signing",
  "public_sign_receipt_accepts_matching_kernel_key",
  "verify_scope_intersection_associative",
  "verify_revocation_predicate_idempotent",
  "verify_delegation_chain_step",
  "verify_receipt_roundtrip",
  "verify_budget_checked_add_no_overflow",
]

[lanes.nightly_only]
description = "Slow Kani harnesses gated to the nightly lane (currently empty; reserved for future slow harnesses)"
harnesses = []

Today lanes.pr contains the full set of fourteen and lanes.nightly_only is empty (reserved for future slow harnesses). The toml comment block at lines 47-62 records the per-harness wall clock used to decide assignment; the script driver scripts/check-kani-public-core.sh reads the file and runs every name in lanes.pr on each PR. Total local wall clock: 134 seconds. The nightly Kani job runs the union of both lanes, so moving a harness from PR to nightly-only strictly reduces PR coverage and never reduces nightly coverage.

Proof-Facing Harnesses

Source: crates/chio-kernel-core/src/kani_harnesses.rs. These target formal_core helpers directly: the time-window classifier, optional and monetary cap subset checks, DPoP admission, budget commits, guard composition, revocation snapshots, and receipt coupling.

• time_window_classifier_matches_valid_predicate · the classifier returns Valid iff issued_at <= now && now < expires_at.
• optional_caps_never_widen_parent_cap · if the parent has a cap and the subset check accepts, the child has the cap and child's value is bounded.
• monetary_caps_never_widen_parent_cap · same shape for monetary caps with currency match.
• dpop_required_missing_or_invalid_fails_closed · DPoP-required admission denies on missing proof, invalid proof, or stale nonce.
• dpop_replayed_nonce_never_admits · replay never succeeds.
• dpop_freshness_rejects_future_beyond_skew · issued_at beyond now+skew is rejected.
• budget_commit_never_increases_remaining_counters · the headline budget property.
• two_sequential_budget_commits_cannot_overspend · two accepted commits cannot together exceed initial remaining.
• guard_deny_or_error_dominates_pipeline · any deny or error in the guard pipeline forces deny.
• revocation_snapshot_denies_presented_token_or_ancestor · denies iff token or any presented ancestor is revoked.
• receipt_coupling_requires_every_field_match · coupling requires capability, request, verdict, policy hash, and evidence class to all match.
• subset_helpers_preserve_parent_requirements · the boolean helpers preserve required-true and never widen.

Coverage

Kani's coverage is by symbol, not by line. The covered_symbols field in formal/rust-verification/kani-public-harnesses.toml lists every symbol a public harness witnesses:

covered_symbols = [
  "chio_kernel_core::verify_capability",
  "chio_kernel_core::NormalizedScope::is_subset_of",
  "chio_kernel_core::scope::resolve_matching_grants",
  "chio_kernel_core::evaluate",
  "chio_kernel_core::sign_receipt",
  "chio_kernel_core::formal_core::optional_u32_cap_is_subset",
  "chio_kernel_core::formal_core::revocation_snapshot_denies",
  "chio_kernel_core::formal_core::monetary_cap_is_subset_by_parts",
  "chio_kernel_core::formal_core::budget_commit",
  "chio_core_types::crypto::PublicKey::verify_canonical",
]

What Kani does not cover: anything outside chio-kernel-core. The async sidecar in chio-kernel, the SQLite-backed receipt store, the HTTP transports, the price oracle, the protocol adapters; none of these has a Kani harness. Their assurance comes from differential tests, fuzz, and the TLA+ revocation propagation spec.

Running

Install Kani via the official installer:

cargo install --locked kani-verifier
cargo kani setup

Run a single harness:

cargo kani -p chio-kernel-core --lib \
  --harness public_evaluate_rejects_untrusted_issuer_before_dispatch \
  --default-unwind 8 --no-unwinding-checks

Run the full public-lane sweep (the PR gate):

./scripts/check-kani-public-core.sh

The script reads formal/rust-verification/kani-public-harnesses.toml and runs every harness in lanes.pr. Output is per-harness pass/fail plus the wall clock.

Reading a Verification Report

A clean Kani report ends with VERIFICATION:- SUCCESSFUL. A failed run ends with VERIFICATION:- FAILED plus a counterexample trace. Each step in the trace shows the symbolic input value at that step and the assertion that triggered.

A typical clean trailer:

SUMMARY:
 ** 0 of N failed (0 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 31.247s

A failed run produces a cbmc_output.txt in target/kani/ with the symbolic state per step. Triage path:

• Reproduce: rerun cargo kani --harness <name> --concrete-playback inplace to embed the counterexample as a regular Rust test.
• Classify: spec bug (the harness asserts something the code is not supposed to satisfy), implementation bug (the code is wrong), harness bug (the assumptions are too weak).
• File via formal/issue-templates/property-counterexample.md and follow the runbook in .planning/trajectory/03-capability-algebra-properties.md.
• Fix and add a regression test that pins the counterexample.

Limits

• Unwind bound. The PR lane uses --default-unwind 8 with --no-unwinding-checks. Loops are not analyzed beyond eight iterations. The harness inputs are constructed so the relevant loops bound at one or two iterations regardless.
• Symbolic state size. Most harnesses use u8 symbolic seeds widened to u64. That gives 256 distinct values per slot; the cross-product across multiple slots is large enough to exercise every branch but small enough to terminate in seconds.
• Concrete fixtures dominate. The two heaviest harnesses (public_verify_capability at 31s, public_evaluate at 28s) exercise the full canonical-JSON serialize plus Ed25519/P-384 verify path with concrete fixture keys. The algebraic harnesses use model_sign/model_verify stubs and finish in 1-3 seconds.
• No alloc semantics. Heap allocation through vec! and String::to_string works inside Kani but is constrained by the symbolic-state size bound. The harnesses that build NormalizedScope values use small concrete shapes plus kani::assume predicates that pin the structure.

P1: capability_monotonicity in this tool

P1 says a child capability's bounds are tighter than its parent's. Kani contributes by symbolically executing the production Rust NormalizedScope::is_subset_of against bounded symbolic inputs and checking that any child that widens the parent is rejected. The directly relevant harness is public_normalized_scope_subset_rejects_value_widened_child, which exercises the cap-widening attack vector. Verbatim from crates/chio-kernel-core/src/kani_public_harnesses.rs:149-185:

#[kani::proof]
fn public_normalized_scope_subset_rejects_value_widened_child() {
    let parent = NormalizedScope {
        grants: vec![NormalizedToolGrant {
            server_id: "s".to_string(),
            tool_name: "r".to_string(),
            operations: vec![NormalizedOperation::Invoke],
            constraints: vec![],
            max_invocations: Some(1),
            max_cost_per_invocation: None,
            max_total_cost: None,
            dpop_required: Some(true),
        }],
        resource_grants: vec![],
        prompt_grants: vec![],
    };
    let child = NormalizedScope {
        grants: vec![NormalizedToolGrant {
            server_id: "s".to_string(),
            tool_name: "r".to_string(),
            operations: vec![NormalizedOperation::Invoke],
            constraints: vec![],
            max_invocations: Some(100),
            max_cost_per_invocation: None,
            max_total_cost: None,
            dpop_required: Some(false),
        }],
        resource_grants: vec![],
        prompt_grants: vec![],
    };

    assume_single_normalized_tool_grant(&child);
    assume_single_normalized_tool_grant(&parent);
    assert!(!child.is_subset_of(&parent));
    core::mem::forget(child);
    core::mem::forget(parent);
}

The harness pins two attack shapes at the same time. The parent has max_invocations: Some(1) and dpop_required: Some(true); the child raises the cap to Some(100) and flips DPoP off with Some(false). The assertion is that child.is_subset_of(&parent) returns false. CBMC unfolds the body of NormalizedScope::is_subset_of on the concrete shapes, and the assume_single_normalized_tool_grant calls pin the structural assumptions so only the bound-comparison path runs. The lane budget is 5 seconds at --default-unwind 8; passing means CBMC found no symbolic execution where the widened child is accepted as a subset.

Two companion harnesses cover the rest of the P1 attack surface. public_normalized_scope_subset_rejects_widened_child catches the case where the child drops a parent constraint (parent has a cap; child has none). public_normalized_scope_subset_rejects_identity_mismatch catches a different-server child. A fourth harness, verify_scope_intersection_associative, runs purely over the algebraic primitive optional_u32_cap_is_subset with three free u32-widened symbolic caps and witnesses transitivity plus reflexivity of the bounded cap lattice.

How this is different from Lean: the Lean theorem proves the bounded model's subset relation does what its definition says, for every input. Kani checks the production Rust's NormalizedScope::is_subset_of against a small symbolic input space at u8 resolution. The Lean proof is unbounded but is over a Lean model; the Kani harness is over the running Rust but only checks the bounded input shapes the harness defines. The Aeneas equivalence theorem closes the gap by proving the bound-comparison primitives in the production source match the Lean bounded model symbol-for-symbol.

Continue the tour at Differential Tests: P1 differential test or jump back to the P1 Tour.

Next

• Theorem Inventory · the proof-to-Rust mapping for every Kani harness.
• Fuzz Infrastructure · the coverage-guided lane that complements bounded model checking.
• Differential Tests · the property-based reference vs production harness.