How to start
1Sign in and get an API keyYour first step is to obtain anImandra Universe API key that your instance of ImandraX will use for connecting.
Goal-state visualization, incremental proof checking and LSP integration. Works out of the box in Cursor and Antigravity.
ImandraX proves properties for all inputs — or finds a concrete counterexample.
Read the full getting started guide here.
Key Features
ImandraX is a cloud-native reasoning engine built for the AI era — foundational infrastructure for AI reasoning and governance that integrates directly into AI agents and automated workflows. Built on decades of research in automated reasoning, it brings mathematical rigor to complex software at scale.
AI Reasoning Infrastructure
ImandraX is foundational infrastructure for AI reasoning and AI governance. Its cloud-native architecture with HTTP API, Python libraries and MCP server allows direct integration into AI agents, enabling them to prove properties, find counterexamples and reason formally.
Automation
Push-button verification designed for engineers, not just Ph.D. researchers. ImandraX's Boyer-Moore-style inductive waterfall handles most proofs fully automatically — and when conjectures are false, it synthesizes concrete counterexamples rather than leaving you stranded.
Counterexamples
ImandraX's reasoning engine is "complete for counterexamples" in a precise sense — including higher-order counterexamples that synthesize functions as witnesses. This goes far beyond what traditional SMT solvers can do.
Imandra Universe
ImandraX is part of Imandra Universe (universe.imandra.ai), an ecosystem of reasoners and neurosymbolic AI integration. CodeLogician, our neuro-symbolic reasoning agent, shows how LLMs and formal reasoning combine to analyze software with mathematical precision.
Extensibility
ImandraX can be customized for particular domains — from financial systems and regulatory compliance to avionics controllers and neural network verification. Its logic is built on OCaml, making models efficiently executable in production.
Meet You Where You Are
Whether you write IML in VS Code, orchestrate proofs from Python notebooks, run verification in CI pipelines, or invoke ImandraX from an AI assistant via MCP — the same reasoning engine is accessible from every context.
Explore the full documentation here.
What ImandraX Can Do
Six core capabilities that set ImandraX apart from conventional testing, SMT solvers and static analysis tools.
Prove & Refute
Automatically prove theorems about your code — or synthesize concrete counterexamples when properties don't hold. Counterexamples are first-class executable values you can inspect and compute with.
Region Decomposition
Decompose the input space of any function into exhaustive, disjoint regions of behavior. A unique capability for test generation, coverage analysis and regulatory compliance.
Cloud-Native & AI-Ready
A multicore, incremental architecture with an HTTP API, Python and OCaml client libraries, and seamless integration with AI agents and LLM-powered workflows.
Interactive Proof Assistant
A rich tactic language with 45+ tactics, a VS Code extension with goal state visualization, and incremental parallel proof checking for fast feedback.
The Inductive Waterfall
A powerful automated proof pipeline inspired by Boyer-Moore: simplification, unrolling, destructor elimination, fertilization, generalization and induction — all working together.
Battle-Tested
Used in production for verifying financial systems, trading algorithms, regulatory compliance engines and safety-critical infrastructure.
Available Plans
Select a plan that scales with your automated reasoning needs, from building AI agents with reasoning skills to deploying enterprise-grade formal verification.
Builder
Built for individual builders who need predictable usage.
Pro
Most PopularFor advanced users running heavier reasoning workloads.
Team
Collaboration and scale for teams shipping reasoning systems.
Core Applications
ImandraX spans formal verification, symbolic reasoning and rule synthesis — all accessible to engineers without requiring formal methods expertise.
Formal Verification
Prove code correct — or find exactly where it breaks
Mathematically verify algorithm properties with push-button automation. ImandraX handles most proofs fully automatically using its Boyer-Moore-style inductive waterfall. When conjectures are false, it synthesizes concrete counterexamples — including higher-order ones that produce functions as witnesses.
Symbolic Reasoning
Map every possible behavior of your system
Decompose the input space of any function into exhaustive, disjoint regions where behavior is invariant — a complete map of all possible outcomes. Solve complex constraints using executable programs as logic, and optimize by searching for solutions that satisfy constraints while minimizing or maximizing a cost function.
Rule Synthesis
Extract auditable logic from complex data and systems
Extract logical patterns from complex, structured and sequential data and synthesize them into a single executable, auditable model. Convert the model into various target languages or prose, detect anomalies in out-of-sample data, and generate corrective actions.
Use ImandraX Your Way
ImandraX meets you where you are — in VS Code, in Python, or via MCP from any AI assistant.
VS Code, Cursor & Antigravity Extension
Goal-state visualization, incremental proof checking, syntax highlighting and type checking via LSP. Works out of the box in Cursor and Antigravity. Install with one command or search "ImandraX" in the Extensions panel.
Python Library
Access virtually every feature of ImandraX with native Python support. Prove properties, synthesize counterexamples, and decompose state-spaces programmatically — ideal for notebooks, CI pipelines, and agent workflows.
MCP Server
Use ImandraX via its own Model Context Protocol server. AI assistants and coding agents (Claude, GPT, Cursor, Gemini) can invoke ImandraX directly — proving properties and finding counterexamples from within a conversation.