Skip to content

kani-verification-kani.md

Latest commit

 

History

History
52 lines (37 loc) · 4.57 KB

kani-verification-kani.md

File metadata and controls

52 lines (37 loc) · 4.57 KB
Raw

Kani Verified Scope — kani-verification (M4 failure-bar demonstration)

Generated by /slo-kani on 2026-05-22. Kani version: 0.67.0 (matches the pinned skills/slo-kani/tools.toml). A green run means "proved within the stated harness, assumptions, and bounds" — never "whole system proved." Concurrency is out of scope for Kani. Demo crate: kerberosmansour/sunlit-kani-demo @ commit c7953f638dd6ddd1a264cbec2842d30ded82482b (built and verified locally; see "Demo repo status" below).

This is the failure-bar evidence: each of four Rust kernels carried a deliberate bug, Kani caught it (red), the documented remediation made it green, all at stated bounds. The catch→remediate→green transition is the proof that the feature is "more stable because of Kani" — a class of bug that was reachable is now provably absent within the harness's scope.

Properties proved (post-remediation)

Harness Target fn Property Verdict
check_zero_prefix zero_prefix no index-out-of-bounds SUCCESSFUL
check_read_byte read_byte safe API: is_some() == (idx < len), no UB SUCCESSFUL
check_accumulate accumulate no overflow; y >= a && y >= b SUCCESSFUL
check_gcd_contract gcd contract holds (requires a!=0 && b!=0 ⇒ no div-by-zero, r != 0) SUCCESSFUL
check_reduce_fraction reduce_fraction caller sound when reusing the verified gcd via stub_verified SUCCESSFUL

Proof scope (per harness)

Harness Bound (unwind / sizes) Assumptions Stubs Contracts Flags
check_zero_prefix unwind(9), fixed [u8; 8] length <= 8 none none (default)
check_read_byte symbolic [u8; 4], symbolic idx none none none (default)
check_accumulate symbolic u32 × u32 (full range) none none none (default)
check_gcd_contract symbolic u8 × u8 (precondition is the contract) none requires(a!=0 && b!=0), ensures(*r != 0), recursion -Z function-contracts
check_reduce_fraction symbolic u8 × u8 a != 0 && b != 0 gcd via stub_verified reuses verified gcd -Z function-contracts -Z stubbing

Catch → remediate → green (naive variant failed first)

Kernel Pre-fix verdict (RED) Kani description Fix Post-fix verdict (GREEN)
K1 zero_prefix FAILURE index out of bounds: the length is less than or equal to the given index (inclusive ..=length writes buffer[8]) exclusive range 0..length SUCCESSFUL @ unwind(9), length <= 8
K2 read_byte FAILURE dereference failure: pointer NULL / one-past-the-end when idx == len (unsafe *xs.as_ptr().add(idx)) safe xs.get(idx).copied() returning Option<u8> + postcondition SUCCESSFUL
K3 accumulate FAILURE attempt to add with overflow (a + b on u32) a.saturating_add(b) + postcondition y >= a && y >= b SUCCESSFUL
K4 gcd FAILURE attempt to calculate the remainder with a divisor of zero / division by zero (no precondition; recursion also expensive) #[kani::requires(a!=0 && b!=0)] + ensures + recursion; caller reuses via #[kani::stub_verified] SUCCESSFUL (contract proof + caller proof)

All four reds were observed BEFORE their greens (the /slo-tla-style naive-first rule), so none of the passing proofs is vacuous.

What remains unproved (disclosed, not eliminated)

  • Bounded ⇒ not unbounded. check_zero_prefix is proved for length <= 8 against a [u8; 8]; check_read_byte for a length-4 slice. These say nothing about larger sizes (accepted residual tm-bounded-proofs).
  • K4 ensures is *r != 0, not full GCD-correctness (no a % r == 0 && b % r == 0) — chosen for reliable, fast verification; the demonstrated property is "the precondition eliminates the div-by-zero class", which is the point.
  • No concurrency claim. These are sequential kernels; interleavings are out of scope for Kani (route to /slo-tla).

Toolchain absence (ENG-1)

The prereq cascade was confirmed: on a machine without cargo kani, the documented loud skip fires (install hints), never a false pass. Here the toolchain was present (cargo-kani 0.67.0), matching the pin, so proofs ran.

Demo repo status

Published. The demo crate is live at https://github.com/kerberosmansour/sunlit-kani-demo @ commit c7953f638dd6ddd1a264cbec2842d30ded82482b (the user ran the gh repo create … --public --push; the commit was re-authored with the GitHub noreply email to satisfy email-privacy protection, which produced this final SHA).