State the seam

The repaired midpoint carries this contract:

#[kani::requires(low <= high)]
#[kani::ensures(|result: &u8| low <= *result && *result <= high)]
fn midpoint(low: u8, high: u8) -> u8 {
    low + (high - low) / 2
}

The precondition is not checked on arbitrary production calls merely because it is written here. In verification, callers must establish it. The postcondition intentionally promises interval containment, not the exact rounding rule; a client that depends on lower-midpoint rounding needs a stronger contract.

Kani 0.67.0 marks function contracts experimental, so enable the feature explicitly:

cargo kani -Z function-contracts --harness midpoint_contract

Compose only after verification

A caller harness may add #[kani::stub_verified(midpoint)]. Kani then avoids re-exploring the implementation and assumes only results allowed by ensures, provided the caller satisfies requires. Preserve two separately checked artifacts:

1. the contract proof over the exact function body and toolchain identity;
2. the caller proof that uses that exact verified contract.

Changing the body, feature set, or contract invalidates the composition until the contract proof runs again. A build graph should encode that dependency rather than relying on a note in a review.

Turn one counterexample into a regression test

Run the broken harness with concrete playback output:

cargo kani --harness buggy_midpoint_stays_in_range --concrete-playback print

Kani prints a Rust unit test containing concrete symbolic choices from the failure. Keep a minimized version beside ordinary tests when it explains the bug. The unit test makes the witness cheap to replay on future builds; it does not replace the symbolic proof, because it covers one assignment only. Regenerate or repair playback when harness control flow changes and consumes symbolic values differently.

Unlike transfer: bounded slicing

Write a function that returns a slice between start and end. Its contract requires start < end <= input.len()= and ensures the result length is end - start. First prove the implementation contract. Then verify a caller's copy loop using a verified stub. Deliberately weaken the postcondition to result.len() < input.len()= and observe which caller proof can no longer be established.

Lessons

• requires is a caller obligation; ensures is a callee promise.
• proof_for_contract checks the real body before composition.
• stub_verified replaces implementation detail with contract-constrained behavior.
• A true but weak contract may be unusable.
• Concrete playback preserves one witness; symbolic verification covers the admitted domain.
• Experimental feature flags and exact tool versions belong in the evidence record.

Practice

1. Retrieval. Which side must establish a precondition?
2. Discrimination. May a generated playback test replace the repaired symbolic harness?
3. Transfer. Complete the bounded-slice contract and caller proof, then weaken the postcondition deliberately.

References

1. Kani. Function contracts. — preconditions, postconditions, contract proof, and verified stubbing
2. Kani. Concrete playback. — generating executable tests from counterexamples