Getting Started

Welcome to ImandraX — foundational infrastructure for AI reasoning and AI governance. Whether you're using ImandraX interactively in VS Code, integrating it into AI agents via its cloud-native API, or building neurosymbolic reasoning workflows through Imandra Universe, this section will take you from zero to writing and verifying your first theorem in just a few minutes.

What you'll learn

1. Installation — Install the VS Code extension (recommended) or the standalone CLI
2. Your First Proof — Write a function, find a counterexample, and prove a theorem
3. The Verification Workflow — From counterexamples to proofs: bounded verification, induction, and interactive tactics
4. Key Concepts — A roadmap of ImandraX's core ideas: the IML language, verification, tactics, and region decomposition
5. VS Code Guide — Master the VS Code extension: goal state viewer, proof navigation, incremental checking

Prerequisites

No prior experience with formal verification or theorem proving is required. If you can write basic functional programs (in OCaml, Haskell, F#, Elm, or similar), you'll feel right at home with ImandraX's modelling language.