What is Imandra?
Imandra is a cloud-native automated reasoning engine for the analysis algorithms bringing unprecedented rigor and automation to algorithm design and governance.
By automated reasoning, we mean automated mathematical techniques combining symbolic (e.g., automated theorem proving) and statistical (e.g., neural networks) AI for performing reasoning tasks such as analyzing all possible behaviors of an algorithm, controller, or synthesizing solutions to complex planning or constraint problems.
By analysis, we mean both mathematically verifying algorithm properties and systematically exploring, enumerating, and elucidating possible algorithm behaviors.
By algorithms, we mean, of course, computer programs, but also virtually any computational system such as planning problems, jet fighter controllers, financial stock exchanges, logistics systems, legal contracts, and autonomous systems.
By cloud-native, we mean Imandra was designed with scalability, seamless cloud-based toolchain integration, and continuous improvement in mind.
Extraction of logical rules from sequential data and anomaly detection
Formal verification, constraint solving, region decomposition
Top features
Over the last decade, there have been many disparate advances in the field of formal verification.
We've spent the last five years carefully crafting an engine that combines these advances into a highly automated reasoning engine for scalable analysis of real-world algorithms.
Unprecedented automation
Traditionally formal verification required a Ph.D. in the domain to be involved because the machines had to be guided to produce results; with Imandra, many in-depth analyses are completely push-button. Moreover, Imandra 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.
Interface languages
Imandra's logic is built directly upon the high-performance functional programming languages OCaml and ReasonML (www.ocaml.org) and (www.reasonml.github.io). This means that Imandra can directly reason about programs written in these languages. Moreover, we've built interfaces for other popular languages.
Extensibility
Imandra's interface languages allow you to express virtually any type of algorithm. Imandra can be further customized for particular domains (e.g., with customized nonlinear decision procedures for analyzing geometrical movements in avionics controllers).
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 Imandra and can be directly computed with and run through the code being analyzed.
Scalability
When analyzing algorithms, many techniques may be performed in parallel and cached. Imandra's cloud-native architecture takes full advantage of this.
Graphical User Interface (GUI)
Imandra’s GUI integration includes Microsoft VS Code (you can download it as a plugin in the Microsoft VS Code Marketplace), Jupyter Notebooks, and is heavily extensible via the Language Server protocol.
Applications
Imandra 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.). Imandra is changing this.
The following are example applications of Imandra 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 Imandra and get results is minimal; indeed, we believe a typical engineering or computer science graduate can easily make serious use of Imandra out of the box.
Verifying a hardware component
Verifying a Robot OS node
We also have several Medium blog posts on the subject:
Imandra interface to Robot OS: Part II
Probabilistic reasoning in ReasonML
Verifying Merge Sort
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.
Read the documentation
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.
Crossing the riverSudoku
OPTIMIZATION - similarly to constraint solving discussed above, Imandra may be used to search for a solution that not only satisfies a specified set of non-trivial constraints.
3. RULE SYNTHESIS
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.
Using Imandra
There are 3 ways to use Imandra: (1) as a stand-alone tool for reasoning about code written in OCaml/ReasonML, (2) creating a Domain-Specific Language (DSL) that translates into OCaml and is analyzed by Imandra, and
(3) by integrating Imandra's Reasoning as a Service® APIs into a larger application:
1. A stand-alone tool for reasoning about code written in OCaml/ReasonML
OCaml is a great open-source general programming language. We have created mechanized formal semantics for its pure subset - code written in this pure subset Imandra automatically translates into axiomatic representation and analyzes. Imandra operates in two "modes" - "logic" for analyzing the pure subset of OCaml and "program," which allows you to write impure OCaml code that
interacts with "logic" mode. This flexibility allows you to write powerful applications leveraging automated reasoning. ReasonML is a new language built on OCaml designed primarily for web development (e.g., Facebook Messenger is written in ReasonML) which Imandra now supports.
2. Create a Domain-Specific Language (DSL) "on top of" Imandra
While OCaml/ReasonML are great general programming languages, many types of problems benefit from Domain-Specific Languages. We have an example of such language - Imandra Protocol Language (IPL).
IPL is a domain-specific language for encoding system connectivity protocols. We designed it primarily for trading systems, but it's generic enough to be applied to any complex system. Our team has incredible language design and development expertise, so if you have a specific project in mind, please do not hesitate to contact us(contact@imandra.ai).
3. Integrate Imandra Core's APIs into another application
Imandra Core's reasoning power may be seamlessly integrated into your application through its Reasoning as a Service® APIs. Imandra Core's features like region decomposition, constraint solving, and optimization (mixing continuous and discrete decision variables) offer unprecedented applications across numerous industries.
One example of such integration is our IPL Simulator product, where a user can turn any IPL (Imandra Protocol Language) model into an on-demand simulation environment. There, Imandra automatically processes the generated model and acts as a library that synthesizes messages in response to user actions.
User Interfaces
VS Code
The Imandra IDE is a VS Code Plugin available for download in the MS Visual Studio Marketplace. It provides the typical syntax highlighting and type checking services and asynchronous reasoning with caching. While you type, Imandra works in the background to analyze the queries and presents the results right back into your editor window. Smart caching of the intermediate results means Imandra is only analyzing incremental changes creating an incredible user experience.
Download VS Code plugin
Jupyter Notebooks
Jupyter Notebook is one of the key interfaces to Imandra. This is particularly useful when using Imandra for data-driven tasks and analyses. Furthermore, a custom printer interface allows you to define HTML printers for Imandra values that the Notebook cells will automatically use.
Terminal
Imandra's command-line interface is the hacker's tool of choice. It provides all of the features, the old school way.
Installation options
1. Single user local Imandra Core
The simplest way to run Imandra Core is by running it on a local machine either as a Docker container or native executables for *nix operating systems (e.g., Mac OS or Linux). Note that this is only available for enterprise and Government users.
2. Single user Imandra Core in a Kubernetes cluster
Imandra is natively designed to take advantage of cloud computing. With Imandra Core running in Kubernetes, it takes advantage of parallelization and caching, significantly speeding up several important classes of queries like region decomposition and formal verification. We provide this as the default environment for our retail customers in Google Cloud and make it available for enterprise and Government users.
3. Multi-tenant Imandra Core in a Kubernetes cluster
Imandra Core caches intermediate results, so running a multi-tenant Kubernetes environment brings further speed improvements as Imandra reuses results from your colleagues' queries. Similarly to the setup #2 above, we provide this for retail customers in the public cloud, enterprise, and government customers (public cloud and on-premise).
