Kani Harnesses
Read a Kani pass by its declared inputs, compiled branch, and unwind bounds before citing it as evidence for a kernel decision.
On this page
Selected authority and accounting decisions in chio-kernel-core satisfy their Kani assertions for every input a harness declares, within the harness’s unwind bounds.
Each pass belongs to its harness: the symbolic or fixed inputs, the compile branch Kani selected, the enabled checks, and the bounds. Creusot contracts, generated equivalence, and differential tests cover the relationships a harness leaves open, and storage IO, journal ordering, concurrent reservations, and snapshot freshness rest on the audited assumptions.
Under cfg(kani), the harness runs the bounded helpers
NormalizedToolGrant::is_subset_of calls is_subset_of_bounded_kani in a Kani build, with bounded operation, constraint, and monetary helpers. The public runner sets default unwind 8, with unwinding checks off except for verify_oracle_inclusion_walk_parity.
A harness declares the inputs, and its assertions state the property
Kani translates a proof harness for checking with CBMC. kani::any introduces symbolic values, kani::assume restricts the inputs considered, and assertions state the property. Some Chio harnesses use symbolic values and others construct fixtures, and a harness name alone does not say which.
The budget harness introduces four symbolic bytes and widens them to u64, so each input ranges from 0 through 255. It calls budget_commit and asserts that neither remaining counter increases, whether the commit is accepted or refused.
Read the budget counter harness
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);
}In the shared budget example, a request costing one invocation and four units moves the counters from (2, 9) to (1, 5). Monotonicity is weaker than the Creusot contract, which states exact deduction and unchanged state on refusal.
Two harnesses cover their whole input domain
The revocation predicate harness chooses two free Booleans: four flag assignments, with no remote store or network delivery. It checks repeated-call equality and the diagonal rule, under which denial equals x when both flags equal x.
| Token revoked | Ancestor revoked | Predicate result |
|---|---|---|
false | false | false · no denial |
false | true | true · denies |
true | false | true · denies |
true | true | true · denies |
The table lists the underlying OR predicate’s decisions; the assertions cover repeated results and the diagonal identity. A passing revocation check is one input to a request’s authorization, which the rest of the evaluation decides.
The settlement-admission harness chooses two four-byte arrays and proceeds only if both decode as UTF-8, along with constraint and delivered-value flags. Under a digest constraint, a non-denial implies a value delivery whose string equals the committed one exactly; constrained non-value delivery denies, and unconstrained delivery is outside the digest check. Its source sets kani::unwind(5). The harness checks string comparison and admission over that domain, while SHA-256 and the payment rail stay outside it; the related Lean inventory entries describe a separate finite delivery model.
Inspect the complete revocation and delivery harnesses
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);
}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 Kani build checks a bounded body of the same method
NormalizedToolGrant::is_subset_of has two compile branches, as the figure draws. An ordinary build iterates in general over operation and constraint membership. Under cfg(kani) it calls is_subset_of_bounded_kani, which uses bounded operation, constraint, and monetary helpers, so a harness calling the method checks the bounded body.
The value-widening fixture builds a parent with invocation cap 1 and required DPoP, and a child that raises the cap to 100 and disables DPoP. The assertion expects the proposed child scope to fail. Both changes sit in one fixture, so the assertion tests them together.
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 fixture restricts both scopes to one tool grant and one operation, with empty constraints, no resource or prompt grants, and no monetary caps, and it removes destructor work with mem::forget. Companion fixtures exercise a removed cap and a server mismatch. The harness named verify_scope_intersection_associative checks transitivity and reflexivity of a scalar cap-subset helper rather than a general scope-intersection operator, so read the assertion and body before turning a harness name into a product claim.
The P1 walkthrough connects this boundary to the attenuation theorem; native differential checks, generated scalar equivalence, and implementation review cover the ordinary path.
Three runners select harnesses by lane, by library, or by manifest
The public registry assigns harnesses to the pr and nightly_only lanes, and all selects their union. Before listing or running, the runner compares the declared names with the proof functions it recognizes in kani_public_harnesses.rs.
- Public core. Runs named public harnesses from the selected
pr,nightly_only, orallset; the default lane ispr. - Core aggregate. Runs the kernel-core library harnesses without a name filter, at default unwind 8 with unwinding checks disabled, then repeats the inclusion-walk harness with unwinding checks enabled. The library includes
kani_harnesses.rs, which checks time windows, cap preservation, budget counters, DPoP facts, guard composition, revocation, receipt coupling, and a reservation-ledger oracle; the runner invokes the library whole rather than the names inkani-harnesses.toml. - Multi-crate manifest. Runs qualified exact harness names with per-entry unwind, feature, and timeout settings. Its
prandnightlylane values select entries, andnightlyselects the entries tagged nightly rather than the union of both lanes.
The multi-crate runner applies the timeout command only when that executable is available. Its list and dry-run modes succeed with an empty selection, and an ordinary empty run fails unless allow-empty is set; read the runner with its manifest. The registry’s logical groups and covered symbols locate related checks, and the property matrix declares which evidence kinds support each formal claim. A catalog entry is a pointer, distinct from line coverage or a call graph.
Inspect the lane assignment and the group and symbol catalogs
[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 = []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",
]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 release records the public lane, and the verdict carries its bounds
The public PR lane runs every registered harness with the runner's settings (default unwind 8, unwinding checks only for the registry's unwinding_checks list) before each release is tagged. The proof report records the lane, its harness count, and its exit against the tag's source commit. Check it for the binary you run:
chio release verify --evidence formalbinary /usr/local/bin/chio chio 0.2.0 aarch64-apple-darwin
checksum matches SHA256SUMS for v0.2.0
signed by release.yml on backbay-labs/chio, issuer token.actions.githubusercontent.com
provenance SLSA v1, 5 subjects, tag v0.2.0
formal proof report bound to v0.2.0, every gate passed
lean root-imported theorems checked
aeneas production extraction and equivalence
kani public PR lane
apalache positive and negative invariants
creusot core contracts
diff-tests scope, canonical JSON, receipts, treaties
timing dudect threshold
verifiedThe kani line is the public lane. To list the registered harnesses, run one focused harness such as verify_revocation_predicate_idempotent, or run the lane after changing kernel code, follow Qualification: formal gates, which pins Kani 0.67.0.
Read the verdict by its kind. A successful verification keeps its harness, input restrictions, compile branch, enabled checks, and bounds. An assertion or safety-check failure yields a counterexample; decide whether the error sits in the implementation, the specification, or the harness assumptions. An unwinding assertion failure means a checked loop needed a larger bound, and a timeout, unsupported feature, or tool failure leaves the result incomplete.
Kani’s concrete playback option turns a supported counterexample into an ordinary Rust regression: print shows it and inplace writes it into the source. A maintainer reproduces with the original package, features, harness, and bounds, and follow Failure Modes for the diagnostic sequence.
A pass holds for the unwind settings it ran with
The public runner supplies default unwind 8 and disables unwinding checks except for verify_oracle_inclusion_walk_parity. With those checks off, success leaves the sufficiency of loop expansion unestablished, and source-level kani::unwind attributes also set bounds; the Kani attribute reference explains the distinction.
An algebraic receipt harness uses model_sign and model_verify with small signer and message identifiers, and other receipt fixtures use a deterministic signing backend; curve implementation correctness rests on ASSUME-ED25519.