← Policy gallery

formalize_before_verify

formal-reasoning reasoning scoped_temporal formal-verificationreasoningordering

Verification goals must be preceded by a formalization step that produced the model being verified.

Formula

G(DefineVG → P_chain Formalize)

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

You cannot verify properties of code that hasn't been formalized into a model first.

Examples

passes Formalize → DefineVG (with formalization in dependency chain)

fails DefineVG with no Formalize action in its artifact lineage

Use it

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