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:

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.

The public lane

The public harnesses live in crates/kernel/chio-kernel-core/src/kani_public_harnesses.rs and are registered in formal/rust-verification/kani-public-harnesses.toml. The two are kept in step mechanically: scripts/check-kani-public-core.sh:167-183 parses every #[kani::proof] function out of the source and exits with source and registry harness sets differ if either side has a name the other does not. A harness added to the file and not to the lane fails the gate, and so does the reverse.

The registry declares one lane that runs and one that is empty:

[lanes.pr]
description = "Kani harnesses run on pull requests touching the scoped paths (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_revocation_admission_projection",
  "verify_delegation_chain_step",
  "verify_receipt_roundtrip",
  "verify_budget_checked_add_no_overflow",
  "verify_budget_admission_projection",
  "verify_reservation_ledger_terminal_classification",
  "verify_reservation_ledger_conservation",
  "verify_composite_quota_all_or_nothing",
  "verify_quota_maximum_immutable",
  "verify_family_binding_preservation",
  "verify_threshold_distinct_signers",
  "verify_delegate_no_widen",
  "verify_delegation_receipt_canonical",
  "verify_revocation_view_freshness",
  "verify_inclusion_step_equivalence",
  "verify_oracle_inclusion_walk_parity",
  "public_delivery_contract_allow_implies_digest_match",
]

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

A pull request that touches the scoped paths runs the kani-public-pr job in .github/workflows/formal-pr-smoke.yml:223-283, which is check-kani-public-core.sh --lane pr behind a path filter. The nightly job kani-public-nightly runs --lane all, the union of both lanes, at .github/workflows/nightly.yml:231. The registry comment at kani-public-harnesses.toml:71-74 records the sizing decision in its own words: the full sweep is about 2.2 minutes locally, inside the 10-minute warm PR target, so every harness lands in lanes.pr.

What the lane covers

The registry catalogs the lane twice over, once by the logical edge or algebraic property each harness exercises:

harness_groups = [
  "public verify_capability fail-closed edges",
  "public NormalizedScope subset edges",
  "public resolve_matching_grants path-prefix edges",
  "public evaluate deny edges",
  "public sign_receipt kernel-key mismatch edge",
  "public sign_receipt WYSIWYS content-hash recompute-and-refuse edge",
  "verify scope intersection associativity (cap-subset transitivity)",
  "verify revocation predicate idempotence",
  "verify revocation admission projection",
  "verify single-step delegation attenuation",
  "verify receipt sign/verify roundtrip algebra",
  "verify budget checked-add no partial commit on overflow",
  "verify composite quota all-or-nothing authorization",
  "verify quota maximum immutability",
  "verify family binding preservation",
  "verify threshold distinct signers",
  "verify recursive delegation no widening",
  "verify delegation receipt canonical-bytes determinism",
  "verify revocation view freshness fail-closed gate",
  "verify inclusion step production-extraction equivalence",
  "verify relying-party inclusion walk soundness under ASSUME-SHA256",
  "verify delivery-contract settlement admission soundness",
  "verify cognition-market challenge award bond cap and exact-sum distribution",
]

And once by the Rust symbols the harnesses witness:

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::revocation_lookup_denies",
  "chio_kernel_core::formal_core::monetary_cap_is_subset_by_parts",
  "chio_kernel_core::formal_core::budget_commit",
  "chio_kernel_core::formal_core::composite_quota_authorize",
  "chio_kernel_core::formal_core::quota_maximum_compatible",
  "chio_kernel_core::formal_core::family_binding_preserved",
  "chio_kernel_core::formal_core::threshold_distinct_eligible_signers",
  "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_core_types::merkle::MerkleProof::compute_root_from_hash",
  "chio_core_types::merkle_steps::inclusion_step",
  "chio_kernel_core::formal_core::delivery_contract_admits",
  "chio_kernel_core::formal_core::delivery_denies_settlement",
  "chio_open_market::finding_slash_amount::compute_slash_allocation",
]

The two catalogs have no declared relation to each other: nothing records which group a harness belongs to, and nothing pairs a group with a symbol. Neither is compared against covered_rust_symbols in formal/proof-manifest.toml either, and the two lists disagree: chio_kernel_core::formal_core::delivery_denies_settlement is a covered symbol here and absent there, while chio_revocation_oracle::api::InclusionProof::verify is a covered symbol there and absent here even though verify_oracle_inclusion_walk_parity is the harness that exercises it.

Worked example: verify_revocation_predicate_idempotent

The smallest harness in the lane, in full:

pub 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, so the predicate carries no hidden state. The mirrored pair pins the diagonal collapse: when the token flag and the ancestor flag coincide, the predicate reduces to a single revocation flag.

Worked example: public_delivery_contract_allow_implies_digest_match

The delivery-contract harness is the one place in the lane where a Kani result and a Lean theorem name the same pair of Rust functions. It is the only harness carrying its own #[kani::unwind(5)], and it bounds both byte strings to four bytes:

pub fn public_delivery_contract_allow_implies_digest_match() {
    let expected: [u8; 4] = kani::any();
    let observed: [u8; 4] = kani::any();
    let (Ok(expected_str), Ok(observed_str)) = (
        core::str::from_utf8(&expected),
        core::str::from_utf8(&observed),
    ) else {
        return;
    };
    let constrained = kani::any::<bool>();
    let delivered_value = kani::any::<bool>();
    let committed = if constrained {
        Some(expected_str)
    } else {
        None
    };

    let denies = delivery_denies_settlement(committed, observed_str, delivered_value);
    if constrained && !denies {
        assert!(delivered_value);
        assert!(expected == observed);
        assert!(delivery_contract_admits(expected_str, observed_str) == DeliveryVerdict::Allow);
    }
    if !constrained {
        assert!(!denies);
    }
    if constrained && !delivered_value {
        assert!(denies);
    }
    if constrained && delivered_value && expected == observed {
        assert!(!denies);
    }

    let retry = delivery_denies_settlement(committed, observed_str, delivered_value);
    assert!(retry == denies);
}

The four assertion groups are the contract stated in both directions. Under a digest constraint, a non-denial forces a value delivery whose observed bytes equal the commitment exactly and forces delivery_contract_admits to return DeliveryVerdict::Allow. An unconstrained delivery is never digest-denied. A constrained non-value delivery always denies, even when its content hash collides with the commitment. And a byte-identical value delivery is always admitted. The final pair of calls pins determinism.

Its Lean counterparts are in formal/lean4/Chio/Chio/Proofs/DeliveryContract.lean. formal/theorem-inventory.json registers three of them, all rootImported: true, claimClass: bounded_model and status: proved:

Two of those three ids appear in P3's matrix row, so P3 is the property this pair of lanes supports. The inventory scopes the first one in its own note: the settlement theorem holds over finite requirement, evidence and opaque digest domains, the Rust linkage covers the digest comparison, and the note says outright that it is not a Rust refinement proof and does not model SHA-256, canonical JSON, signatures, persistence, payment rails, or external settlement. The Kani harness closes the digest half of that gap over four-byte strings; nothing here reaches the payment rail.

Proof-facing harnesses

A second set of harnesses lives in crates/kernel/chio-kernel-core/src/kani_harnesses.rs and targets the formal_core helpers directly: the time-window classifier, the optional and monetary cap subset checks, DPoP admission, budget commits, guard composition, revocation snapshots and receipt coupling. Its registry is formal/rust-verification/kani-harnesses.toml, whose status is core_harnesses_required_for_strict_ci and whose two commands are ./scripts/check-kani-smoke.sh and ./scripts/check-kani-core.sh.

The twelve property harnesses:

• 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.

Two more sit in the same file and are oracle comparisons rather than single properties. scalar_helpers_match_reference_predicates checks the formal_core scalar helpers against reference predicates written beside them, and reservation_ledger_matches_one_step_oracle checks ledger_apply against a one-step transition oracle defined at the top of the file. The manifest note at formal/proof-manifest.toml:237 places that second one in context: reservation conservation has four independent enforcement surfaces, and this harness is one witness on the pure transition, with the manifest recording in its own words that production ledger linkage is not established.

What the lanes reach

Kani coverage here is declared by symbol, not measured by line. Three registries declare it and they do not have the same scope:

The multi-crate manifest carries its own relation to the public-core one in a comment at .kani/harnesses.toml:20-23: its chio-kernel-core entries mirror the public-core PR lane, and scripts/tests/check-kani-public-core.test.sh fails if the two lists drift. Each [[harness]] block there pins its own default_unwind, timeout_secs and lane, which is where a per-harness bound lives; the public-core runner has one bound for the whole lane.

What no Kani harness reaches: the async sidecar in chio-kernel, the SQLite-backed receipt store, the HTTP transports, the price oracle, and the protocol adapters. The manifest's note at formal/proof-manifest.toml:236 draws the same line for the budget and revocation harnesses in particular: they verify shared scalar projection functions called by both production backends, and they do not verify storage IO, mutation journals, snapshot freshness, or reservation-ledger transitions.

Reproduce

The lane needs cargo-kani. CI installs it pinned: CHIO_KANI_VERSION is set to the same value in .github/workflows/formal-pr-smoke.yml, nightly.yml and proof-mutants.yml, and each job runs cargo kani --version as its own step before proving anything.

cargo install --locked kani-verifier --version "$CHIO_KANI_VERSION"
cargo kani setup

List the lane without invoking Kani, which needs no toolchain at all:

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

Run the lane. The script builds each cargo kani invocation from the registry, so a harness name never has to be typed:

# the PR lane
./scripts/check-kani-public-core.sh --lane pr

# the union of both lanes, which is what the nightly job runs
./scripts/check-kani-public-core.sh --lane all

A clean run ends with Kani public core harnesses passed followed by the harness count and the lane name (check-kani-public-core.sh:228). One harness at a time, the invocation the script would issue is:

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

Drop --no-unwinding-checks for verify_oracle_inclusion_walk_parity, the sole entry in the registry's unwinding_checks list. That harness keeps CBMC's unwinding assertions on, so a loop that needed more iterations than the bound allows fails the run instead of passing quietly.

Reading a verification report

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

On a failure, triage in this order:

• Reproduce with cargo kani --harness <name> --concrete-playback inplace, which embeds the counterexample as an ordinary Rust test.
• Classify: a spec bug (the harness asserts something the code is not supposed to satisfy), an implementation bug (the code is wrong), or a harness bug (the kani::assume constraints are too weak).
• File with formal/issue-templates/property-counterexample.md. A liveness counterexample from the temporal lanes has its own template beside it.
• Fix, then add a regression that pins the counterexample so it cannot come back silently.

Limits

• Unwind bound. The lane runs at --default-unwind 8, so loops are not analyzed beyond eight iterations. Harness inputs are built so the relevant loops bound at one or two regardless. Every harness but one also runs with --no-unwinding-checks, which means a loop that did need more than eight iterations would be truncated rather than reported. verify_oracle_inclusion_walk_parity is the exception and keeps the checks on; public_delivery_contract_allow_implies_digest_match overrides the bound in source with #[kani::unwind(5)].
• 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 clock. The registry comment at kani-public-harnesses.toml:66-74 records why: public_verify_capability and public_evaluate exercise the full canonical-JSON serialise plus Ed25519 and P-384 verify path, while the algebraic harnesses model signatures with model_sign and model_verify and finish in one to three seconds.
• Modelled crypto. The signature algebra those stubs stand in for is spelled out in the source comment above model_sign: a signature over (signing key, message) verifies under (verifying key, message) exactly when the keys are paired and the message matches. Nothing in the receipt-roundtrip harness reaches a real curve.
• 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 in this lane

P1 is capability attenuation: a delegated capability can only narrow. Kani's contribution is to run the production Rust NormalizedScope::is_subset_of on symbolic inputs and check that a child which widens the parent on any axis is rejected. The harness that pins the cap-widening shape is:

pub 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 once. 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. The two assume_single_normalized_tool_grant calls pin the structural assumptions so only the bound-comparison path runs, and the two core::mem::forget calls keep the drop glue out of the symbolic execution.

Three companion harnesses cover neighbouring shapes. public_normalized_scope_subset_rejects_widened_child catches a child that drops a parent cap entirely. public_normalized_scope_subset_rejects_identity_mismatch catches a different-server child. verify_scope_intersection_associative runs over the algebraic helper optional_u32_cap_is_subset with three symbolic caps and witnesses transitivity plus reflexivity. The full delegation step, all 22 axes of it, is verify_delegation_chain_step, walked through on the P1 tour.

Lean and Kani carry different boundaries here, and neither subsumes the other. The Lean theorem holds for every input in its domain but that domain is a Lean model. The Kani harness runs the shipped Rust but only over the input shapes the harness constructs, and the concrete-fixture harnesses like this one pin two values rather than exploring a space. The Aeneas equivalence theorems connect the two for the registered extraction symbols and for nothing else.

See also

• 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.