Tutorials

These tutorials walk you through real verified algorithms step by step. Each one teaches specific ImandraX concepts and techniques while producing a complete, correct proof.

Prerequisites

Before starting these tutorials, you should be comfortable with:

• Installing ImandraX and creating .iml files
• Basic IML syntax — functions, types, pattern matching
• The concept of verification commands — verify, theorem, lemma

Tutorial progression

The tutorials are ordered from introductory to advanced:

1. Sorting Algorithms — Verify that insertion sort produces sorted output with the right elements. Concepts: induction, rewrite rules, automatic proofs.

2. Merge Sort — Verify merge sort with both automatic and manual tactic proofs. Concepts: custom termination measures, forward-chaining rules, manual tactics.

3. Compiler Verification — Verify a compiler from expressions to a stack machine. Concepts: custom induction schemes, compiler correctness.

4. Ripple-Carry Adder — Prove correctness of a hardware adder circuit. Concepts: hardware verification, bit vectors, automatic proofs of complex properties.

5. Majority Vote — Prove the Boyer-Moore MJRTY voting algorithm correct. Concepts: using lemmas, algorithm verification, uniqueness proofs.

6. Interactive Proofs — Learn to use the VS Code goal state viewer to develop proofs interactively. Concepts: tactic composition, step-by-step proof development.