← Policy gallery

formalization_is_analyzed

formal-reasoning reasoning scoped_temporal reasoningformal-verificationworkflow

Every formalized model is either verified or analyzed — no model is built and left unused.

Formula

G(Formalize → F(Verify ∨ StateSpaceAnalysis))

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 formalization that is never verified or decomposed is dead weight — building a model only pays off when the model is actually reasoned over, so an unused Formalize is a flagged gap.

Examples

passes Formalize(model) → Verify(model) (or StateSpaceAnalysis(model)) later in the trace

fails Formalize(model) with no subsequent Verify or StateSpaceAnalysis

Use it

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