ImandraX

available

imandrax

formal verification Imandra generalfix-certification

The automated reasoning engine: a prover for IML that decides verification goals, returns proofs or counterexamples (sat models), and computes region decompositions. It is the engine under IPL / Imandra Connectivity — decomposing a formalized FIX Rules-of-Engagement model into an exhaustive set of symbolic regions, one per certification case, from which a conformance suite is generated.

Produces

VerificationResultDecomposition

The trace artifacts this reasoner emits — the evidence a policy can require.

Capabilities

proofscounterexamplesdecision proceduresregion decomposition

Learn more

https://www.imandra.ai/ ↗

Policies using ImandraX

Policies whose verification evidence is produced by this reasoner.

ipl_cert_cases_from_decomposition ipl-fix-certification

Certification Cases Generated by Region Decomposition

ipl_cert_cases_selected ipl-fix-certification

Certification Cases Appropriately Selected

ipl_cert_invalid_flows_tested ipl-fix-certification

Invalid Flows Exercised

In a policy

Policies reference a reasoner with the reasoner field — e.g. require that a high-stakes change carry a VerificationResult produced by imandrax before commit. See the policy gallery.