> For the complete documentation index, see [llms.txt](https://dsg-3.gitbook.io/dsg-docs/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://dsg-3.gitbook.io/dsg-docs/agi-simulation/kani-harness-skeleton.md).

# Kani Harness Skeleton

Copy this into a Kani-enabled test module when Kani is installed.

```rust
#[cfg(kani)]
mod proofs {
    use rust_core::core::*;

    const N: usize = 4;
    const M: usize = 4;

    #[kani::proof]
    fn prove_total_fail_closed_no_panic() {
        let current: State<N> = kani::any();
        let proposed: State<N> = kani::any();
        let policy: Policy<M> = kani::any();

        let _ = process_transition(&current, &proposed, &policy);
    }

    #[kani::proof]
    fn prove_forbidden_always_blocks() {
        let current: State<N> = kani::any();
        let proposed: State<N> = kani::any();
        let policy: Policy<M> = kani::any();

        kani::assume(valid_state(&current));
        kani::assume(valid_state(&proposed));
        kani::assume(valid_policy(&policy));
        kani::assume(contains_forbidden_state(proposed.name_id, &policy));

        let result = process_transition(&current, &proposed, &policy);

        assert_eq!(result.decision, Decision::Block);
    }

    #[kani::proof]
    fn prove_same_state_zero_drift() {
        let state: State<N> = kani::any();

        kani::assume(valid_state(&state));

        let drift = compute_drift(&state, &state).unwrap();

        assert_eq!(drift, 0);
    }

    #[kani::proof]
    fn prove_drift_symmetry() {
        let a: State<N> = kani::any();
        let b: State<N> = kani::any();

        kani::assume(valid_state(&a));
        kani::assume(valid_state(&b));

        let ab = compute_drift(&a, &b).unwrap();
        let ba = compute_drift(&b, &a).unwrap();

        assert_eq!(ab, ba);
    }
}
```