Apply Formal Methods Where It Makes Sense — ponens Policy Pack

This pack governs the pragmatic adoption of formal methods: use a theorem prover (ImandraX) exactly where correctness is high-stakes and machine-checkable, and — once formal methods are in play — run the pipeline rigorously end to end. It is authored by Imandra for the CodeLogician / SpecLogician formal-reasoning workflow.

Source: Imandra — CodeLogician / SpecLogician formal-reasoning pipeline.

Why this maps onto ponens

Formal methods pay off unevenly. Proving everything is wasteful; proving nothing is negligent for the code that actually carries risk — money math, state machines, access control, bounds, parsing. This pack encodes where to apply formal effort and how to apply it well, as computable policies over the reasoning trace.

The pack has two halves:

Coverage — “where it makes sense”. High-stakes code must be backed by a proof or a region decomposition in its lineage before it ships. The high-stakes surface is data-driven: a producer sets the trace’s high_stakes_paths (e.g. from a formalization-target scan that scores money / state-machine / access-control code), so “where it makes sense” is decided by evidence, not hard-coded paths.
Rigor — “do it properly”. Once the pipeline runs, it must run correctly: verification goals are formalized first, refuted goals get fixed, decompositions produce tests, and generated tests trace back to a decomposition.

Formal methods	ponens
The formal-reasoning session record	the trace
A discipline of the pipeline	a policy (temporal formula)
Hard requirement vs good practice	`error` (Red) / `warning` (Amber)
The code that warrants a prover	`high_stakes_paths` on the trace

Trace model

Reuses the existing formal-reasoning vocabulary — actions Formalize, DefineVG, Verify, Decompose, GenerateTests, EditFile; artifacts IMLModel, VerificationResult, Decomposition, GeneratedTests; predicates proved, sat, refuted, and the data-driven high_stakes_path. No new action types.

Policies

Coverage — apply where it matters

Policy	Sev	Formula
`reasoning_required_for_high_stakes`	error	`G(EditFile ∧ high_stakes_path → P_chain(VerificationResult(proved ∨ sat) ∨ Decomposition))`

Rigor — a proper pipeline

Policy	Sev	Formula
`formalize_before_verify`	error	`G(DefineVG → P_chain Formalize)`
`counterexample_triggers_fix`	warning	`G(Verify ∧ refuted → F(EditFile))`
`decomposition_drives_tests`	warning	`G(Decompose → F(GenerateTests))`
`generated_tests_require_decomposition`	error	`G(GeneratedTests → Decomposition ∈ ancestors(derived_from))`

How “high-stakes” is decided

high_stakes_path matches an action’s target against the trace’s high_stakes_paths list (substring match), falling back to demo defaults when the field is absent. A formalization-target scan is the natural producer: it scores which functions warrant ImandraX and writes their files into high_stakes_paths, so this pack’s coverage requirement tracks the same opportunities the scan surfaces.