KZ-9: 7 contracts missing proof_obligations, falsification_tests, kani_harnesses

[noahgift]

Kaizen Finding: KZ-9

Source: /kaizen aprender run 2026-03-18
Severity: Medium
Gate: K8 (contract lint)

Problem

7 contracts have equations but are missing proof infrastructure (proof_obligations, falsification_tests, kani_harnesses). pv lint fails: 0/3 gates passed.

Affected Contracts

• apr-cpu-q4k-routing-v1 — missing proof_obligations, falsification_tests, kani_harnesses
• element-wise-ops-v1 — missing proof_obligations, falsification_tests, kani_harnesses
• matvec-kernel-v1 — missing proof_obligations, falsification_tests, kani_harnesses
• normalization-kernel-v1 — missing proof_obligations, falsification_tests, kani_harnesses
• rope-kernel-v1 — missing proof_obligations, falsification_tests, kani_harnesses
• softmax-kernel-v1 — missing proof_obligations, falsification_tests, kani_harnesses
• transpose-kernel-v1 — missing proof_obligations, falsification_tests, kani_harnesses

Five-Whys

1. Why no proof infrastructure? Contracts were scaffolded with equations only.
2. Why equations only? pv scaffold generates stubs but obligations require domain knowledge.
3. Why weren't they filled in? Time pressure — equations were prioritized over proofs.
4. Why not caught earlier? No kaizen cycle existed to lint contracts.
5. Why not? This is the first kaizen run.

Fix

For each contract, add:

1. proof_obligations matching each equation's invariants
2. falsification_tests with if_fails descriptions
3. kani_harnesses with bounded model checking stubs

Use the provable-contracts softmax-kernel-v1 contract as a reference template.