Organizations / Imandra
Imandra
Imandra (Aesthetic Integration) · www.imandra.ai/
Imandra builds automated reasoning for safety-critical systems. Its Imandra Protocol Language (IPL) formalizes a trading venue's Rules of Engagement as a precise, executable model — from which Imandra Connectivity derives conformance test suites, on-demand simulators, certification reports and drift monitoring. This pack captures the best practice for certifying counterparties against a FIX specification using IPL.
How the publications map to ponens policies
IPL compresses a venue's near-infinite FIX state space into a finite set of symbolic regions via the ImandraX reasoner's Region Decomposition; each region becomes one certification case the counterparty must pass. Where IPL establishes *whether* a counterparty conforms, ponens governs *that the certification process was actually followed* — the Rules of Engagement were formalized and version-pinned as an IPL model, the certification cases were generated from the model's regions (not hand-written), an appropriate subset was selected and justified (with invalid and rejection flows kept in scope), every failing case was resolved, and no counterparty reached production without a passed, reported certification.
Each stage of the Imandra Connectivity workflow — formalize the ROE, generate tests, certify (Simulator or Proxy), co-simulate against live traffic, and monitor for drift — becomes a policy group evaluated by ponens trace check over the certification trace. A divergence between the IPL specification and a live session is the observable failure the digital twin is designed to surface, raised here as an error-severity policy.
Apply Formal Methods Where It Makes Sense
Put ImandraX to work exactly where correctness is high-stakes and machine-checkable — and, once formal methods are in play, use them rigorously end to end.
A curated pack for teams adopting formal methods pragmatically. It has two halves. COVERAGE: high-stakes code (the paths a formalization-target scan flags — money math, state machines, access control, bounds) must be backed by a proof or a region decomposition in its lineage before it ships, so formal effort lands where it pays off rather than everywhere. RIGOR: once the pipeline runs, it must run properly — verification goals are formalized first, refuted goals get fixed, decompositions produce tests, and generated tests trace back to a decomposition. The 'high-stakes surface' is data-driven via the trace's high_stakes_paths, so 'where it makes sense' is decided by evidence, not hard-coded paths.
Source: Imandra — CodeLogician / SpecLogician formal-reasoning pipeline.
Rigorous pipeline 7
counterexample_triggers_fix warning Counterexample Triggers Fix
When a verification goal is refuted (counterexample found), a fix action should follow.
G(Verify ∧ refuted → F(EditFile))decomposition_drives_tests warning Decomposition Drives Tests
A region decomposition should be followed by generated tests, so the behavioral breakdown actually yields high-coverage checks rather than being left unused.
G(Decompose → F(GenerateTests))formalization_is_analyzed warning Formalization Is Analyzed
Every formalized model is either verified or analyzed — no model is built and left unused.
G(Formalize → F(Verify ∨ StateSpaceAnalysis))formalize_before_verify error Formalize Before Verify
Verification goals must be preceded by a formalization step that produced the model being verified.
G(DefineVG → P_chain Formalize)generated_tests_require_decomposition error Generated Tests Require Decomposition
Generated test artifacts must derive from a Decomposition artifact in their lineage.
G(GeneratedTests → Decomposition ∈ ancestors(derived_from))refuted_results_must_be_reproved error Refuted Results Must Be Re-Proved
A refuted verification result offered as evidence must ultimately be resolved into a proved/sat result — not merely edited around. This is the quality-of-evidence check behind the goal's GOVERNED axis: a criterion is MET the moment a VerificationResult exists for its component, but the result must actually establish the property to count as governed.
G(VerificationResult(refuted) → F(VerificationResult(proved ∨ sat)))verified_claims_are_fidelity_checked warning Verified Claims Are Fidelity-Checked
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).
(F SourceCode) → G(Verify → F(ConformanceResult(passed)))FIX Certification with IPL
Best practice for certifying a counterparty against a venue's FIX specification using IPL — formalize the Rules of Engagement as an IPL model, generate the certification cases by region decomposition, certify in Simulator or Proxy mode, and monitor for drift — as computable policies over the certification trace.
Imandra Connectivity certifies a counterparty's FIX implementation against a venue's Rules of Engagement (ROE) by formalizing the ROE as an Imandra Protocol Language (IPL) model, then deriving everything downstream from it: the certification cases — generated from the IPL model by the ImandraX reasoner's Region Decomposition — plus on-demand simulators, a certification report, and continuous drift monitoring. This pack encodes the best practices of that workflow as deterministic checks over the certification trace — the ROE must be a valid, version-pinned IPL model; the certification cases must be generated from the model's symbolic regions and an appropriately selected, justified subset run (covering invalid flows and risk-prioritised regions — not every case, and not an arbitrary few); certification must run in a declared mode and produce a report; every failing region must be resolved; the model must be co-simulated against live traffic before sign-off; and no counterparty reaches production without a passed certification, after which spec-vs-system drift must surface as an observable failure. `ponens trace check` turns the per-policy verdicts into a single certification gate.
Source: Imandra Connectivity / IPL — Imandra Protocol Language for formalizing FIX Rules of Engagement (https://www.imandra.ai/connectivity, https://ipl.dev).
ROE Formalization in IPL 3
ipl_cert_model_valid error IPL Model Valid Before Generation
The IPL model must type-check and be free of errors before it is used to generate tests or simulators — only a valid model is guaranteed to produce a functioning implementation.
G(GenerateTests → P(ipl_model_valid))ipl_cert_model_version_pinned error IPL Model & ROE Version Pinned
A certification sign-off must pin the exact IPL model version and the ROE version it formalizes, so the result is traceable to a specific formal specification.
G(CertificationSignoff → ipl_model_version_pinned ∧ roe_version_pinned)ipl_cert_roe_formalized error ROE Formalized in IPL
The venue's Rules of Engagement / FIX specification a counterparty is certified against must be formalized as an IPL model — an executable formal spec — before any certification run, not left as prose.
G(CertificationRun → P(Formalize ∧ ipl_model_formalizes_roe))Case Generation & Selection 3
ipl_cert_cases_from_decomposition error Certification Cases Generated by Region Decomposition
The certification cases a counterparty is tested against must be generated from the IPL model by region decomposition — each case traceable to a symbolic region of the model — rather than hand-written ad hoc.
G(CertificationCase → P_chain(RegionDecomposition ∧ ipl_model_valid))ipl_cert_cases_selected error Certification Cases Appropriately Selected
Region decomposition produces far more cases than can be executed exhaustively. Certification must run a deliberately selected subset of the generated cases — justified by a documented selection strategy and covering the required behaviour classes and risk-prioritised regions — not every generated case, and not an arbitrary few.
G(CertificationSignoff → P(case_selection_justified ∧ required_classes_covered))ipl_cert_invalid_flows_tested error Invalid Flows Exercised
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.
G(CertificationSignoff → P(invalid_flows_selected ∧ invalid_flows_tested))Certification & Onboarding 4
ipl_cert_defects_resolved error Failing Cases Resolved Before Sign-off
Certification cannot be signed off while any selected certification case is failing; every conformance failure — whether in the counterparty or in the IPL model — must be resolved and re-run first.
G(CertificationSignoff → ¬open_conformance_failure)ipl_cert_mode_declared warning Certification Mode Declared
Each certification run must declare its mode — Simulator (against an IPL-generated simulator) or Proxy (in-line with the live venue) — so its scope and fidelity are on the record.
G(CertificationRun → certification_mode_declared)ipl_cert_no_onboarding_without_pass error No Onboarding Without a Passed Certification
No counterparty is enabled in production without a prior IPL-based certification that passed and was signed off.
G(EnableProduction → P(CertificationSignoff ∧ passed))ipl_cert_report_produced error Certification Report Produced
A completed certification run must produce a certification report tying each verdict back to the IPL model's regions; a run that finishes with no report is not an auditable certification.
G(CertificationComplete → F(certification_report_produced))Digital Twin & Drift Detection 2
ipl_cert_drift_monitored error Production Drift Surfaced & Resolved
In production, live sessions must be checked against the IPL model; any drift between specification and running system must surface as an observable failure and be resolved or raised as an incident.
G(drift_detected → F(drift_resolved ∨ Incident))ipl_cert_model_cosimulated warning Model Co-simulated Against Live Traffic
Before sign-off the IPL model should be co-simulated against captured UAT or production traffic (the digital twin) to confirm the model and the real system agree.
G(CertificationSignoff → P(model_cosimulated ∧ consistent))