Invalid Flows Exercised

error

ipl_cert_invalid_flows_tested

fix-certification conformance pure_temporal iplimandrafix-certificationtest-generationvalidation

Whatever subset of cases is selected, it must include invalid and rejection behaviour, not just happy paths — the IPL model's invalid message flows (validity violations and the expected reject responses) must be among the cases exercised.

Formula

G(CertificationSignoff → P(invalid_flows_selected ∧ invalid_flows_tested))

Hover any operator or symbol for what it means.

Requires a reasoner

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

Why it matters

Case Generation & Selection. ImandraX can enumerate invalid flows (e.g. @@invalidOnly / @@includeInvalid regions) — messages that violate validity constraints and the rejections they should provoke. Because the run is a selection rather than the full set, invalid-flow cases must be deliberately kept in scope; certifying only valid paths leaves a counterparty's rejection handling unverified, the most common source of production surprises.

Examples

passes Invalid-message regions tested → counterparty returns the correct reject → CertificationSignoff

fails CertificationSignoff with only valid order flows tested and no invalid/reject regions

Use it

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