Overview
What's ImandraX?
ImandraX is the latest version of our automated reasoning engine for the analysis of algorithms bringing unprecedented rigor and automation to algorithm design and governance.
How it works:
ImandraX is a reasoning engine for algorithms expressed in IML (Imandra Modeling Language), a "pure" subset of OCaml (www.ocaml.org) with a set of reasoning directives. It automatically translates IML into mathematical logic and uses "symbolic AI" (or automated reasoning) to reason about it using precise logical steps, always explaining its rationale with independently auditable output. You can use it from VS Code, via Python libraries and now, via its own MCP server.
How to start:
• Obtain Imandra Universe API Key here
• Download VS Code Extension here
Learn more
DocumentationKey Features
Automated reasoning, including formal verification, has seen incredible breakthroughs over recent years. We've leveraged these deep advances to design ImandraX, an industrial-strength reasoning platform for verifying complex software at scale. With powerful proof automation, a seamless integration of bounded and unbounded verification, first-class counterexamples and state-space region decompositions, ImandraX brings the power of formal verification to mainstream software engineers.
Automation
Traditionally use of advanced automated reasoning techniques in industrial settings (e.g. formal verification) required a Ph.D. in the domain to be involved because the machines had to be guided to produce results; with ImandraX, many in-depth analyses are completely push-button. Simply put, ImandraX is designed with the engineer in mind. For example, ImandraX has a seamless integration of bounded model-checking and full-featured interactive theorem proving, giving users the freedom to choose how deep they'd like to go (in terms of state-space exploration) on various algorithm analysis tasks, with verification explanations that can be directly incorporated into safety and audit cases.
Counterexamples
Imandra's reasoning engine is "complete for counterexamples" in a precise sense. Verification practitioners are well aware that one of the largest time sinks in verification comes from trying to prove false goals. With Imandra, we set out to eliminate this issue in a practical sense by building a reasoning engine that can synthesize deep counter-examples to incorrect verification conjectures automatically, even in the presence of recursive functions and nonlinear arithmetic. Moreover, as Imandra's logic is built on an executable programming language, all counterexamples are made "first-class" in ImandraX and can be directly computed with and run through the code being analyzed.
Interface language
ImandraX's logic is built directly upon the high-performance open-source functional programming language OCaml Imandra Modeling Language (IML) is essentially the "pure" subset of OCaml and additional directives for reasoning. When analyzing IML, ImandraX converts the code into mathematical representing using a mechanized formal semantics we've developed for the "pure" subset of OCaml.
Extensibility
Imandra's interface languages allow you to express virtually any type of algorithm. ImandraX can be further customized for particular domains (e.g., with customized nonlinear decision procedures for analyzing geometrical movements in avionics controllers).
Scalability
ImandraX is designed with scalability in mind. Models are efficiently executable OCaml programs which can be used directly in production or easily turned into efficient simulators and auditors. Reasoning leverages deep advances in automated theorem proving and counterexample synthesis, including a lifting of SMT to computational higher-order logic with recursion and induction. ImandraX proofs are composed from a robust and ergonomic collection of tactics, and can be orchestrated both automatically and interactively.
User Interfaces
ImandraX has a powerful and intuitive VS Code Extension (available here), a new Python library (install here) and now MCP server (read here) for easy integration with AI assistants and agents.
Applications
ImandraX has three core applications: formal verification, symbolic reasoning, and rule synthesis:
1. Formal Verification
FV is a well-established field built around the mathematical verification of algorithm properties. Historically, and especially as applied to general software verification, this was a very manual effort requiring years of specialized training (Ph.D.). ImandraX is changing this.
The following are example applications of ImandraX verifying properties from different domains. You will notice that 1) you use the same language to write programs and properties you wish to verify, and (2) the level of FV expertise required to use ImandraX and get results is minimal; indeed, we believe a typical engineering or computer science graduate can easily make serious use of ImandraX out of the box.
2. Symbolic Reasoning
State-Space Decomposition
Region Decomposition is inspired by Cylindrical Algebraic Decomposition, a fundamental technique for reasoning about nonlinear polynomial systems by decomposing Euclidean space into a finite number of connected regions s.t. within each region, the behavior of the system under analysis is invariant. This effectively computes a "map" of all possible behaviors of the system and facilitates a wide variety of nonlinear decision procedures over the reals and complexes.
Constraint Solving
Some problems require much more powerful means of expressing than what traditional constraint solvers provide. Imandra treats code as mathematical logic, allowing you to encode even the most complex problems as executable programs, which can then be automatically analyzed with respect to a rich language of constraints (including recursive functions, higher-order functions).
Optimization
Similarly to constraint solving discussed above, ImandraX may be used to search for a solution that not only satisfies a specified set of non-trivial constraints, but maximizes/minimizes specified cost function.
3. Rule Synthesis
Extracting Logical Patterns
With Imandra, you can extract logical patterns from complex structured, sequential data and synthesize them into a single, executable and auditable model. You can further convert the model into various target programming languages and English-prose and ask in-depth questions about its behavior. The model may be used to identify anomalies in out-of-sample data and generate corrective actions to rectify any detected issues. Rule synthesis has applications in many industries and technologies, including financial services and RPA (Robotic Process Automation). For example, as part of our partnership with Itiviti, Imandra"s Rule Synthesis feature is used to migrate legacy client connectivity systems.
User Interfaces
VS Code / Cursor
The ImandraX VS Code Extension is now available for download in the MS Visual Studio Marketplace. It provides the typical syntax highlighting and type checking services and asynchronous reasoning with caching. It also "works out of the box" in the Cursor IDE.
VS Code Extension
Python library
ImandraX has a completely new Python library! Access virtually every feature of ImandraX with native Python support!
Python Library
MCP
You can now use ImandraX via its own MCP server! If you're using an AI-assistant IDE like Cursor, this will be an invaluable tool!
MCP
