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.
User Interfaces
A powerful VS Code Extension with goal state visualization and incremental proof checking, Python libraries for programmatic access, and an MCP server for seamless integration with AI assistants and agents.
What's ImandraX?
How it works:
ImandraX reasons about algorithms expressed in IML (Imandra Modeling Language), a "pure" subset of OCaml with reasoning directives. It automatically translates IML into mathematical logic and uses symbolic AI (automated reasoning) to prove properties, synthesize counterexamples and decompose behavior — always with independently auditable output. Its cloud-native architecture with HTTP API, Python libraries and MCP server means it integrates directly into AI agents and automated workflows. Our neuro-symbolic reasoning agent CodeLogician demonstrates how LLMs and formal reasoning combine to analyze software with mathematical precision.
Three Core Applications
ImandraX has three core applications spanning formal verification, symbolic reasoning, and rule synthesis — all accessible to engineers without requiring formal methods expertise.
Formal Verification
Mathematically verify algorithm properties with push-button automation. ImandraX handles most proofs fully automatically — and when conjectures are false, it synthesizes concrete counterexamples, including higher-order ones that produce functions as witnesses.
Symbolic Reasoning
Decompose state-space into regions where system behavior is invariant — a complete map of all possible behaviors. 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 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 Extension
Goal-state visualization, incremental proof checking, syntax highlighting and type checking via LSP. Works out of the box in Cursor. 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.
CodeLogician
Our neurosymbolic reasoning agent, built on ImandraX — combining LLM coding agents with formal reasoning to systematically analyze software behavior, catch edge cases, and ship with confidence instead of guesswork.
Trusted by leading institutions