1 Introduction

Imandra is a modern computational logic theorem prover built around a pure, higher-order subset of OCaml. Mathematical models and conjectures are written as executable OCaml programs, and Imandra may be used to reason about them, combining models, proofs and counterexamples in a unified computational environment. Imandra is designed to bridge the gap between decision procedures such as SMT [2], semi-automatic inductive provers of the Boyer-Moore family like ACL2 [1, 6], and interactive proof assistants for typed higher-order logics [4, 5, 7, 8]. Our goal is to build a friendly, easy to use system by leveraging strong automation in proof search that can also robustly provide counterexamples for false conjectures. Imandra has novel features supporting large-scale industrial applications, including a seamless integration of bounded and unbounded verification, first-class computable counterexamples, efficiently executable models and a cloud-native architecture supporting live multiuser collaboration. Imandra is already in use by major companies in the financial sector, including Goldman Sachs, Itiviti and OneChronos [9].

Fig. 1.
figure 1

An example Imandra session illustrating recursive definitions, computable counterexamples ( ), bounded verification ( ), unbounded verification with automated induction ( ), and higher-order instance synthesis.

Full size image

An online version may be found at https://try.imandra.ai (Fig. 1).

2 Logic

Imandra’s logic is built on a mechanized formal semantics for a pure, higher-order subset of OCaml. Foundationally, the subset of OCaml Imandra supports (called the ‘Imandra Modelling Language’) corresponds to a (specializable) computational fragment of HOL equivalent to multi-sorted first-order logic with induction up to \(\epsilon _0\) extended with theories of datatypes, integer and real arithmetic. Theorems are implicitly universally quantified and expressed as Boolean-valued functions. Proving a theorem establishes that the corresponding function always evaluates to . As in PRA (Primitive Recursive Arithmetic) and Boyer-Moore logics, existential goals are expressed with explicit computable Skolem functions [1, 3, 11].

2.1 Definitional Principle

Users work with Imandra by incrementally extending its logical world through definitions of types, functions, modules and theorems. Each extension is governed by a definitional principle designed to maintain the consistency of Imandra’s current logical theory through a discipline of conservative extensions. Types must be proved well-founded. Functions must be proved terminating. These termination proofs play a dual role: Their structure is mined in order to instruct Imandra how to construct induction principles tailored to the recursive function being admitted when it later appears in conjectures.

Imandra’s definitional principle is built upon the ordinals up to \(\epsilon _0\). Ordinals are encoded as a datatype ( ) in Imandra using a variant of Cantor normal form, and the well-foundedness of —the strict less-than relation on values—is an axiom of Imandra’s logic.

To prove a function f terminating, an ordinal-valued measure is required. Measures can often be inferred (e.g., for structural recursions) and may be specified by the user. To establish termination, all recursive calls of f are collected together with their guards, and their arguments must be proved to conditionally map to strictly smaller ordinals via the measure. Imandra provides a shorthand annotation for specifying lexicographic orders ( ), and explicit measure functions may be given using the annotation.

Example 1 (Ackermann)

We can define the Ackermann function and prove it terminating with the attribute which maps to the ordinal \(m\cdot \omega + n\). Alternatively, we could use to give an explicit measure via helper functions in Imandra’s module.

figure n

Example 2

Here we have a naive version of the classic left-pad function [13], where termination depends on both arguments in a non-lexicographic manner:

figure o

2.2 Lifting, Specialization and Monomorphization

Imandra definitions may be polymorphic and higher-order. However, once Imandra is tasked with determining the truth value of a conjecture, the goal and its transitive dependencies are transformed into a family of ground, monomorphic first-order (recursive) definitions. These transformations include lambda lifting, specialization and monomorphization. Imandra’s supported fragment of OCaml is designed so that all admitted definitions may be transformed in this way.

Example 3

To prove the following higher-order theorem

figure p

we obtain a set of lower level definitions, where the anonymous function was lifted, the type was monomorphised, and and were specialised:

figure t

3 Unrolling of Recursive Functions

A major feature of Imandra is its ability to automatically search for proofs and counterexamples in a logic with recursive functions. When a counterexample is found, it is reflected as a first-class value in Imandra’s runtime and can be directly computed with and run through the model being analysed. In fact, the statement does not try any inductive proving unless requested; the default strategy is recursive function unrolling for a fixed number of steps, a form of bounded symbolic model-checking.

Our core unrolling algorithm is similar in spirit to the work of Suter et al. [12] but with crucial strategic differences. In essence, Imandra uses the assumption mechanism of SMT to block all Boolean assignments that involve the evaluation of a (currently) uninterpreted ground instance of a recursive function. A refinement loop, based on extraction of unsat-cores from this set of assumptions, then expands (interprets) the function calls one by one until a model is found, an empty unsat-core is obtained, or a maximal number of steps is reached.

Definition 1 (Function template)

A function template for f is a set of tuples \((g, \mathbf {t}, \mathbf {p})\) such that the body of f contains a call to \(g(\mathbf {t})\) under the path \(\mathbf {p}\).

Example 4

 

  • \(\textsf {fact} (x)= \textsf {if}~x > 1~(x * \textsf {fact} (x-1))~1\) has as template \(\{ (\textsf {fact} , \mathbf {(x-1)}, (x>1)) \}\)

  • \(f(x) = 1 + \textsf {if}~g(0)~h(g(x))~h(42)\) has as template \(\{ (g, (0), \top ), (h, \mathbf {(g(x))}, (g(0)=\top )), (g, \mathbf {(x)}, g(0)=\top ), (h, \mathbf {(42)}, (g(0)=\bot )) \}\)

We use what we call reachability literals to prevent the SMT solver from picking assignments that use function calls that are not expanded yet. A reachability literal is a Boolean atom that doesn’t appear in the original problem, and that we associate to a given function call \(f(\mathbf {t})\) regardless of where it occurs. This is to be contrasted with Suter et al.’s notion of control literals associated with individual occurrences of function calls within the expanded body of another function call. We denote by \(\textsf {b}[f(\mathbf {t})] \) the unique reachability literal for \(f(\mathbf {t})\).

Fig. 2.
figure 2

Unrolling algorithm

Full size image

The main search loop is presented in Fig. 2, where \(body_f\) is the body of f (i.e. \(\smash { f(\mathbf {x}) \mathrel {\overset{\text {\tiny def}}{=}} body_f }\)) and \(t \triangleleft u\) means t is a proper subterm of u. We start with F initialized to the original goal, and the queue q containing function calls in the goal (computed by ). Each iteration of the loop starts by checking validity under the assumption that all reachability literals in q are false (line 11). If no model is found, we pick an unexpanded function call \(f(\mathbf {t})\) from the unsat core (line 15). Selection must be fair: all function calls must eventually be picked.

To expand \(f(\mathbf {t})\), the corresponding reachability literal becomes true, we instantiate the body of f on \(\mathbf {t}\), and use to compute the set of subcalls along with their control path within \(f(\mathbf {t})\) (using f’s template). For each \(\textsf {b}[g(\mathbf {u})] \) occurring under path p inside \(\smash { \textsf {body}_f(\mathbf {t}) }\), we need to block models that would make p valid until \(g(\mathbf {u})\) gets expanded. The assertions \(\bigwedge _i \left( b[f(\mathbf {t})] \wedge p_i \mathrel {\Rightarrow } a_i \right) \) delegate to SMT the work of tracking which paths are forbidden. This way, expanding one function call might lead to many paths becoming “unlocked” at once.

Fig. 3.
figure 3

Imandra’s inductive waterfall

Full size image

4 Induction

Imandra has extensive support for automated induction built principally around Imandra’s inductive waterfallFootnote 1. This combines techniques such as symbolic execution, lemma-based conditional rewriting, forward-chaining, generalization and the automatic synthesis of goal-specific induction principles. Induction principle synthesis depends upon data computed about a function’s termination obtained when it was admitted via our definitional principle. Imandra’s waterfall is deeply inspired by the pioneering work of Boyer-Moore [1, 6], and is in many ways a “lifting” of the Boyer-Moore waterfall to our typed, higher-order setting (Fig. 3).

Imandra’s waterfall contains a simplifier which automatically makes use of previously proved lemmas. Once proved, lemmas may be installed as rewrite, forward-chaining, elimination or generalization rules. Imandra gives users feedback in order to help them design efficient collections of rules. With a good collection of rules (especially rules), it is hoped that “most” useful theorems over a given domain will be provable by simplification alone, and induction will only be applied as a last resort. In these cases, the subsequent waterfall moves are designed to prepare the simplified conjecture for induction (via, e.g., generalization) before goal-specific induction principles are synthesized.

Imandra’s inductive waterfall plays an important role in what we believe to be a robust verification strategy for applying Imandra to real-world systems. Recall that all Imandra goals may be subjected to bounded verification via unrolling (cf. Sect. 3). In practice, we almost always attack a goal by unrolling first, attempting to verify it up to a bound before we consider trying to prove it by induction. Typically, for real-world systems, models and conjectures will have flaws, and unrolling will uncover many counterexamples, confusions and mistakes. As all models are executable and all counterexamples are reflected in Imandra’s runtime, they can be directly run through models facilitating rapid investigation. It is typically only after iterating on models and conjectures until all (bounded) counterexamples have been eliminated that we consider trying to prove them by induction. Imandra’s support for counterexamples also plays another important role: as a filter on heuristic waterfall steps such as generalization.

5 Architecture and User Interfaces

Imandra is developed in OCaml and integrates with its compiler libraries. Arbitrary OCaml code may interact with Imandra models and counterexamples through the use of Imandra’s program mode and reflection machinery. Imandra integrates with Z3 [2] for checking satisfiability of various classes of ground formulas. Imandra has a client-server architecture: (i) the client parses and executes models with an integrated toplevel; (ii) the server, typically in the cloud, performs all reasoning. Imandra’s user interfaces include:

  • Command line for power users, with tab-completion, hints, and colorful messages. This interface is similar in some ways to OCaml’s .

  • Jupyter notebooks hosted online or via local installation through Docker [10]. This presents Imandra through interactive notebooks in the browser.

  • VSCode plugin where documents are checked on the fly and errors are underlined in the spirit of Isabelle’s Prover IDE [14].

6 Conclusion

Imandra is an industrial-strength reasoning system combining ideas from SMT, Boyer-Moore inductive provers, and ITPs for typed higher-order logics. Imandra delivers an extremely high degree of automation and has novel techniques such as reflected computable counterexamples that we now believe are indispensible for the effective industrial application of automated reasoning. We are encouraged by Imandra’s success in mainstream finance [9], and share a deep conviction that further advances in automation and UI—driven in large part by meeting the demands of industrial users—will lead to a (near-term) future in which automated reasoning is a widely adopted foundational technology.