v3.8.0 — Provable Contracts Integration

Provable Contracts Integration

Escape-proof contract enforcement pipeline across the entire sovereign AI stack. YAML contracts → build.rs env vars → #[contract] proc macro → debug_assert!() injection. Zero runtime cost in release builds.

New Compliance Checks

Check	What it verifies
CB-1203	Contract equations with preconditions have #[contract] macros
CB-1204	build.rs emits PRE/POST env vars from YAML contracts
CB-1205	Provability invariant: proof_obligations → kani_harnesses + tests
CB-1206	Verification level distribution (L2/L4/L5 from proof-status.json)
CB-1207	Contract drift detection (90-day staleness via git log)

Scoring Integration

• pv score D1-D5 dimensions replace custom formula (spec_depth, falsification, kani, lean, binding)
• proof-status.json parsed for actual L4/L5 coverage ratios
• #[contract] macro count feeds into formal verification scorer
• lean_theorem: references in YAML give partial Lean credit to consumer repos

New CLI Features

• pmat comply --format sarif — SARIF output for GitHub Code Scanning (delegates to pv lint)
• pmat query --contracts — Cross-project contract search (delegates to pv query)

Stack Integration

8 repos wired with full escape-proof contract pipeline:
trueno (27), entrenar (11), realizar (11), aprender (75), simular (3), forjar (5), rmedia (3), presentar (3) — 138 total contracts, 90 #[contract] macros

Kani Verification

3 proofs verified: relu_nonneg (2.9s), relu_monotonic (8.7s), softmax_positivity (5.3s). stub_exp tightened to [MIN_POSITIVE, 1.0] matching Lean-proven exp bounds.

Stats

• 21,665 tests, 0 failures
• 0 clippy warnings
• COMPLIANT
• 86.6/100 Grade B