[kreneskyp]

Summary

Add the V2 checked-clause LLVM analyzer for the observation portions of FR-004-AC-16..24. It derives the clause population and implication count from the admitted CheckedPackageV2, checks the generated source and map against that population, and classifies bounded LLVM evaluation and consequent probes. Malformed or incomplete evidence returns structured non-success without a fabricated classification. AC-18's binding refusal remains planned and has no test trace in this PR.

The public observation report carries a versioned format marker and a strict JSON schema. Its integration tests validate each emitted success and refusal shape against that schema.

The analyzer reports observations only. Native-run binding and proof-credit decisions remain separate under FR-004-AC-10..15.

Evidence

• Tests-first commits cover clause population, changed and missing maps, all four classifications in one admitted package, malformed LLVM input, aggregate byte limits, and a real LLVM run whose consequent is skipped.
• A separate tests-first commit requires the versioned observation schema; the implementation follows it.
• Focused tests: 10/10 passed on the rebased head. Focused Clippy passed before rebase.
• Pre-PR full make ci passed in both configurations (378 library tests, 675 integration tests, and 16 doctests in each). Real make kani-gate passed 37/37 on the pre-rebase tree. The rebase adds unrelated merged Kani changes; the exact final head will receive the second full gate before merge.

Review

Non-author code/Rust review and gap analysis are recorded in SR-14362 and SR-14363. Their AC-18 traceability findings were fixed and dispositioned at d5c0b65; the validated artifacts are committed unchanged in reviews/.