ponens

← Reasoner registry

Imandra CodeLogician

available

codelogician

formal verification Imandra generalpaymentsstate-machines

Translates code into IML and proves properties — or finds counterexamples — over the resulting model, with region decomposition and exhaustive test generation.

Produces

IMLModelVerificationGoalVerificationResultDecompositionGeneratedTests

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

Capabilities

proofscounterexamplesregion decompositiontest generation

Learn more

https://www.imandra.ai/ ↗

Policies using Imandra CodeLogician

Policies whose verification evidence is produced by this reasoner.

decomposition_drives_tests apply-formal-methods
Decomposition Drives Tests
formalize_before_verify apply-formal-methods
Formalize Before Verify
reasoning_required_for_high_stakes apply-formal-methods
Reasoning Required for High-Stakes Changes
refuted_results_must_be_reproved apply-formal-methods
Refuted Results Must Be Re-Proved

In a policy

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