Kani Harnesses

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 exercising branches reachable at that resolution in budget_commit. The two assertions are the property: a successful commit cannot increase either remaining counter.

Public Harnesses

Source: crates/kernel/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, plus the delegation and revocation surfaces capability::delegate, DelegationReceipt::canonical_bytes, RevocationView::install_if_newer, and InclusionProof::verify.

The documented public harnesses use the lane-wide bound --default-unwind 8 --no-unwinding-checks from scripts/check-kani-public-core.sh. The lane-assignment note in formal/rust-verification/kani-public-harnesses.toml records the timing that keeps every harness in lanes.pr: the concrete-fixture harnesses dominate the runtime while the algebraic ones finish in one to three seconds (Kani 0.67.0).

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:

[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",
  "public_sign_receipt_refuses_content_hash_mismatch",
  "public_sign_receipt_accepts_matching_content_hash",
  "verify_scope_intersection_associative",
  "verify_revocation_predicate_idempotent",
  "verify_delegation_chain_step",
  "verify_receipt_roundtrip",
  "verify_budget_checked_add_no_overflow",
  "verify_delegate_no_widen",
  "verify_delegation_receipt_canonical",
  "verify_revocation_view_freshness",
  "verify_oracle_inclusion_soundness",
]

[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 twenty and lanes.nightly_only is empty (reserved for future slow harnesses). Despite the lane name, no Kani job runs on an ordinary PR today: the driver scripts/check-kani-public-core.sh reads the file and runs every name in lanes.pr inside the nightly kani-public-nightly job (the union of both lanes) and again in the release-qualification Kani lane. The full sweep is roughly 2.2 minutes locally, inside the six-minute budget the lane is sized for; moving a harness to nightly_only would strictly reduce that lane and never reduce nightly coverage.

Proof-Facing Harnesses

Source: crates/kernel/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",
  "chio_core_types::capability::delegate",
  "chio_core_types::delegation_receipt::DelegationReceipt::canonical_bytes",
  "chio_kernel_core::revocation_view::RevocationView::install_if_newer",
  "chio_revocation_oracle::api::InclusionProof::verify",
]

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 nightly and release-qualification 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/kernel/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 additional P1 input cases. 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 over the algebraic helper optional_u32_cap_is_subset with three free u32-widened symbolic caps and witnesses transitivity plus reflexivity of the bounded cap lattice.

Lean and Kani use different models and boundaries. The Lean theorem establishes the model's subset relation for its domain. 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. Aeneas equivalence theorems relate listed extracted helpers to the handwritten model. They do not establish equivalence for all production code or input shapes.

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.