Verification
Verification is the heart of ImandraX. It's where you move from writing code to proving that your code is correct — or discovering exactly how it fails.
ImandraX combines three complementary approaches:
- Bounded verification (unrolling) — Symbolic model checking with built-in decision procedures. Fast, fully automatic, and excellent at finding counterexamples.
- Unbounded verification (the inductive waterfall) — A sophisticated proof engine that combines simplification, induction, and multiple proof strategies to establish properties for all inputs.
- Interactive proof construction — A rich language of reasoning tactics and tacticals that allows you to ergonomically guide the system, construct proofs step by step, and explore counterexamples interactively.
The recommended workflow is: start with bounded verification to search for counterexamples — most conjectures are false, and unrolling finds this quickly. Iterate on fixing your models and goals until no counterexamples remain, then prove the goal with [@@by auto] or other tactics. ImandraX won't attempt induction unless you ask for it via a tactic.
ImandraX supports a spectrum of proof styles: highly automated declarative proofs built from a sequence of lemmas and definitions that the waterfall orchestrates automatically, and tightly controlled interactive proofs constructed from a precise sequence of tactics with fine-grained control over every step.
In this section
- Commands — The five core commands:
verify,instance,theorem,lemma,axiom - Tactics — The unified tactic language with 45+ composable tactics
- Subterm Selection — A pattern language for picking subterms from proof goals
- Simplification — Rewrite rules, forward chaining, and the simplifier
- Unrolling — Bounded model checking and counterexample synthesis
- Induction — Functional and structural induction
- The Waterfall — The full automated proof pipeline
- Counterexamples — Working with synthesized counterexamples
- Termination — Proving functions terminate and why it matters
- Incremental Proofs — Parallel and incremental proof checking