← Policy gallery

verified_claims_are_fidelity_checked

formal-reasoning conformance scoped_temporal conformancefidelityformal-verification

Every verification of a model TRANSLATED FROM CODE should be backed by a passed model↔code fidelity check — a verdict is fully code-grounded only when the model provably reproduces the real code. Vacuous for spec-first / authored IML (no source to conform to).

Formula

(F SourceCode) → G(Verify → F(ConformanceResult(passed)))

Hover any operator or symbol for what it means.

Requires a reasoner

This policy is satisfied by verification from codelogician — an automated-reasoning tool in the reasoner registry.

Why it matters

A proof holds of the MODEL. When the model was translated from real code, a fidelity (conformance) check is what links the two — without it a 'verified' verdict is only provisional and may not reflect the deployed system. The requirement is guarded by `F SourceCode` so it applies only when there IS source to conform to: a spec-first / authored-IML session (no SourceCode artifact) passes vacuously, since the IML itself is the artifact, not a translation. Fidelity is optional in the current flow, so a missing check on code-derived models is a flagged gap, not a hard failure (hence warning).

Examples

passes Verify(model) → ConformanceResult(passed) linking the model to the real code

fails Verify(model) with no passed fidelity/conformance check

Use it

ponens policies add verified_claims_are_fidelity_checked --into ./trace.json
ponens trace check ./trace.json