Imandra
Core

At Imandra, our mission is
to revolutionize algorithm design,
regulation, transparency and governance
by democratizing automated reasoning.

Our mission

Fundamentally, the algorithms we depend on have become too complex to design and implement ‘by hand.’ The problem is that the mathematical tools available to do this right — formal verification and automated reasoning — have classically been inaccessible to those without a PhD in the field and have often not scaled to relevant "real-world" problems.

We founded the company to change this. Based upon deep advances in (both symbolic and statistical) AI, we’ve built Imandra to make automated reasoning scalable and accessible.

What is Imandra?

Imandra is a cloud-native automated reasoning engine for analysis of 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 or 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, autonomous systems, etc.

By cloud-native we mean Imandra was designed with scalability, seamless cloud-based toolchain integration and continuous improvement in mind.

What’s special about Imandra?

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.

Let us briefly go through some of the distinct features of Imandra:

Unprecedented automation - traditionally formal verification required a PhD in the domain to be involved because the machines had to be guided to produce results; with Imandra, many deep 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.org). This means that Imandra can directly reason about programs written in these languages. Moreover, we’ve built interfaces for other popular languages such as Python.

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 counterexamples 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.

What does Imandra do?

Let’s now dive into the specifics with links to various interactive examples. As already discussed, Imandra has two core applications: formal verification and symbolic reasoning. Here we present both with relevant examples:

1. FORMAL VERIFICATION

FV is a well-established field built around the mathematical verification of algorithm properties. Historically, and especially as it’s applied to verification of general software, this was a very manual effort requiring years of specialized training (PhD). Imandra is changing this.

The following are examples 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 an typical engineering or computer science graduate can easily make serious use of Imandra out of the box.

Verifying a simple vehicle controller
Verifying a hardware component
Verifying a Robot OS node

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 a high-level overview ...

Here are some of the use cases:

Testing - when it comes to testing complex systems, everyone agrees that they should be tested ‘thoroughly’, but what does that mean? What’s a scientifically-grounded technique for describing ‘thoroughness’? With Region Decomposition, you get precisely this - a quantitative measure of a system state-space. The Regions in this case represent the quantitative analogs of ‘edge cases’ that engineers typically construct ‘by hand’ or with help of random number generators.

Model-based engineering - Imandra paves way to true model-based development (MBE). A model developed in Imandra is:
● Susceptible to formal verification as discussed above
● Executable, so may be co-simulated with the actual implementation to audit performance
● May be used to automatically generate test cases with quantitative coverage metrics, through the application of Imandra’s Region Decomposition machinery.

Autonomous systems - as autonomous systems become ubiquitous, it is evermore important to ensure they’re tested thoroughly. Reliable simulation environments are used to test algorithms before they’re deployed in the real-world. But the question remains: how do we reason about thoroughness of the tests that these systems are subjected to? With Imandra, you may develop a model of the physical environment and derive the symbolic edge cases (or regions), and translate them into testing scenarios targeting specific simulation environments.

Example: Simple Stoplight Model


Explainability/Documentation generation - when Imandra computes regions, it reflects them back into the runtime so you may compute with them. We have example where we translate region descriptions into English-like prose which may serve as precise and automatically generated documentation of a model. In fact, our clients in financial services already rely on this technique for generating up-to-date and thorough documentation.



Reinforcement learning - when you’re training an image classifier, it’s important to make sure the training data is diverse. No single class is over-represented or under-represented. Any skew in the training data will lead to a bias in the classifier. How do we translate this to decision controllers trained using Reinforcement learning? Imandra’s Region Decomposition provides a methodology for ensuring the training of reinforcement learning algorithms is diverse. Naturally, this leads to better performance and faster convergence. We have results to demonstrate this which we can share if you’re interested. Moreover, we have developed a Python interface (discussed below) to make it easy to use Imandra together with the popular NN libraries like TensorFlow.

Planning - in complex domains, it may be the case that there are no ‘good’ solutions and the operator has to choose one among many and understand why those options were presented. Imandra is uniquely positioned to not only solve both traditional and highly nontraditional planning problems (e.g., through its decision procedures for recursive function unrolling integrated with SMT solving), but also to leverage its symbolic reasoning to explore, compare and explain the full spectrum of possible outcomes and generate concrete plans to accomplish them.

CONSTRAINT SOLVING - some problems require much more powerful means of expressing problems 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, nonlinear real and floating point arithmetic and more):

Examples of Imandra solving constraints:

Crossing the river
Sudoku



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, but also maximizes (or minimizes) a specific penalty function. We will have examples of these solutions soon.

How can you use Imandra?

There are two ways to use Imandra: (1) as a stand-alone tool for reasoning about your code written in OCaml/ReasonML, and (2) by incorporating its Reasoning as a Service APIs within a larger application:

1. Write code in OCaml/ReasonML - analyze it with Imandra (e.g. verify its properties) and then use the OCaml/ReasonML compiler toolchain to compile the code to an executable.




2. Using Imandra’s APIs in a larger software - use Imandra as a “powerful calculator”. For example, one application may be for a planning system where the user interface would compose the problem and ask Imandra to solve it.

As a back-end for reasoning about algorithms written in OCaml/ReasonML or a Domain Specific Language (DSL).

Some problems require special languages for describing and reasoning about them. We have 2 examples of domain-specific languages developed as a front-end to Imandra to deal with specific domains. What’s special about these DSLs is that they have a formal semantics defined in Imandra - that is, a syntactically valid program written in the DSLs can be automatically translated into Imandra code that Imandra can reason about.

There are currently two DSLs:

IDF-Py - a Python interface to our Iterative Decomposition Framework (Region Decomposition optimized for analysis of multi-step behavior of state machines). We created the Python interface to make this easily accessible for machine learning/AI developers.

IDF-Py Documentation


Imandra Protocol Language (IPL) - domain specific language for specifying connectivity protocols. We designed this primarily for trading systems, but it’s generic enough that it may be applied to any complex communication protocols.

IPL Documentation

We have considerable expertise in developing domain-specific languages so don’t hesitate to ask if you have a particular domain that would benefit from this.

Imandra compared to other systems and techniques

Boyer-Moore: Like ACL2, Imandra’s logic is based on a mechanized formal semantics for an efficiently executable programming language (for ACL2, this is a first-order fragment of Lisp; for Imandra, this is a higher-order fragment of OCaml/ReasonML). This means that Imandra models are simultaneously executable programs (i.e., valid OCaml/ReasonML) and mathematical artifacts which may be subjected to rigorous formal analysis by Imandra’s reasoning engine. In Imandra, we have “lifted” many core Boyer-Moore ideas powering their remarkable successes in automating induction and simplification to our typed, higher-order setting.

HOL, Isabelle/HOL, Coq, Agda and Lean: Like provers in the HOL family (as well as those based on dependent types such as Coq, Agda and Lean), Imandra’s logic is strongly typed. Like HOL systems, Imandra is built upon a higher-order polymorphic type theory (a variant of Hindley-Milner corresponding to pure OCaml). Imandra supports a rich executable fragment of HOL, with automation including efficient higher-order rewriting and induction through first-order specialization.

SAT and SMT: Like SMT solvers, Imandra contains orchestrated combinations of high-performance CDCL-based SAT solving and decision procedures for theories relevant to program analysis. Crucially, Imandra’s proof procedures support the synthesis of reflected executable counterexamples (even of higher-order goals requiring function synthesis). All counterexamples constructed by Imandra are “first-class,” i.e., executable and available in the same runtime environment as the formal models themselves. This allows rapid prototyping iteration and model diagnostics, as counterexamples can be directly run through models. Imandra lifts SMT from (non-executable, monomorphic) first-order logic without recursion and induction to a rich executable, polymorphic higher-order logic with recursion and induction.

Integration of Model Checking and Theorem Proving: Imandra seamlessly integrates bounded model checking (lifted to operate modulo higher-order recursive functions over algebraic datatypes, integers, reals, etc.) and “full-fledged” interactive theorem proving. Every verification goal in Imandra may be analyzed in “bounded” and “unbounded” fashions, and bounded results may be turned into actual theorems (e.g., incorporating bounds on the datatypes involved explicitly in theorem hypotheses) automatically. This allows for powerful incremental approaches to verification, utilizing bounded verification to rapidly eliminate design flaws,“completing” the results to their unbounded form as necessary only after all flaws corresponding to counterexamples found by bounded verification attempts have been eliminated.

Nonlinear Decision Procedures for Hybrid Systems: Imandra has deep support for datatypes and decision procedures relevant to the analysis of hybrid systems. This includes model-producing decision procedures for the existential theory of real closed fields (nonlinear real arithmetic w.r.t. systems of many-variable nonlinear polynomial equations and inequalities) integrated with Imandra’s inductive “waterfall” proof procedure. Moreover, Imandra can natively compute with and reason about real algebraic numbers. Through our experience working with (and in many cases contributing to) hybrid systems verification tools such as KeYmaera, Flow*, dReal and dReach and HybridSAL, we recognize scalable nonlinear real decision procedures as one of the most important bottlenecks in hybrid systems verification. The derivation of computable counterexamples (dually, instances in the case of test-case generation) satisfying constraints on both the discrete and continuous components of the models is crucial to efficient V&V.

Details on Region Decomposition

Region decomposition lifts CAD to algorithms through a combination of symbolic execution, automated induction and nonlinear decision procedures. The result is an automatic method for decomposing the state-space of a system (as given by the “step” function of an (infinite) state-machine) into a finite number of symbolically described regions s.t. (a) the union of all regions covers the entire state-space, and (b) in each region, the behavior of the system is invariant. Regions decompositions are computed subject to a basis, a collection of function and predicate symbols which are taken as “basic” and will be used in region descriptions, and side-conditions which may express queries to focus the decomposition on specific behaviors (i.e., compute all regions of the state-space s.t. the controller will result in the following bad state). Bases and side-conditions facilitate configurable abstraction boundaries and foci and allow the analysis of the state-space to be adapted for many different applications, from high-coverage test-suite generation to automated documentation synthesis to interactive state-space exploration.

Give it a spin

Try Imandra

and join us on

Discord
By using this website, you agree to our cookie policy

Please note that the Imandra website no longer supports Internet Explorer

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox