Core Features
Key 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.
Automation
Traditionally, industrial use of automated reasoning techniques has required a formal verification Ph.D. to guide formal verification tools. With ImandraX, many in-depth analyses are completely push-button. Simply put, ImandraX is designed with the engineer in mind.
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.
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.
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.
User Interfaces
ImandraX has a powerful and intuitive VS Code Extension, a new Python library and now MCP server for easy integration with AI assistants and agents.
About
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.