Welcome to Imandra!¶
Imandra is both a programming language and a reasoning engine with which you can analyse and verify properties of your programs.
As a programming language, Imandra is a subset of the functional language OCaml. We call this subset of OCaml “IML” or “ImandraML” (for “Imandra Modelling Language”).
With Imandra, you write your code and verification goals in the same language, and pursue programming and reasoning together.
Imandra has many advanced features, including firstclass computable counterexamples, symbolic model checking, support for polymorphic higherorder recursive functions, automated induction, a powerful simplifier and symbolic execution engine with lemmabased conditional rewriting and forwardchaining, firstclass statespace decompositions, decision procedures for algebraic datatypes, floating point arithmetic, and much more.
Before starting to use Imandra, it may be helpful to read this short Introduction.
This section will give you a quick, 5 minute overview of what Imandra can do. If you want to play around with the code in any of the examples hit the 'Try this!' buttons throughout, and you'll get a Jupyter notebook session where you can experiment. (If you got here via try.imandra.ai, you're already in one of these notebook sessions  if that's the case just run the cells using the Jupyter controls!)
Your first proof and counterexample¶
Let's define a couple of simple arithmetic functions and analyse them with Imandra:
let g x =
if x > 22 then 9
else 100 + x
let f x =
if x > 99 then
100
else if x < 70 && x > 23
then 89 + x
else if x > 20
then g x + 20
else if x > 2 then
103
else 99
val g : Z.t > Z.t = <fun> val f : Z.t > Z.t = <fun>
Here, g
and f
are the names of our functions, and they each take a single
integer argument x
. In Imandra,
let g x = <body>
is the equivalent of something like
function g (x : Int) { <body> }
in many other languages.
Notice how we did not have to declare the type of x
in the definition of f
and g
. Imandra's type system has inferred that x
is an integer automatically
from how x
is used. Sometimes it's advantageous to annotate our definitions
with types manually. We could write this explicitly by defining g
with an
explicit type annotation, e.g.,
let g (x : int) = <body>
As f
and g
are functions, we can of course compute with them:
However, functions in Imandra are more than just code: they're also mathematical objects that can be analysed and subjected to the rigours of mathematical proof.
For example, let's verify that for all possible integer inputs x
, g x
never goes above 122
, which corresponds to the logical statement
(forall (x : int), g x <= 122)
. We represent logical statements like these with OCaml
functions:
Now let's ask Imandra to verify our statement!
verify g_upper_bound
 : Z.t > bool = <fun>
ground_instances:  0  
definitions:  0  
inductions:  0  
search_time:  0.012s  
details:  Expand

start[0.012s] (if ( :var_0: ) > 22 then 9 else 100 + ( :var_0: )) <= 122
simplify
into: true
expansions: []
rewrite_steps: forward_chaining:  Unsat
Imandra has verified this fact for us automatically, by directly examining the
definition of our statement and the definitions of the other functions it refers
to (in this case, g
).
Now, let's ask Imandra to verify that there exists no x
such that f x
is
equal to 158
. Giving our statements names can sometimes be a bit unwieldy
(although it can be helpfully descriptive in some situations). For simple
statements like these, the statements themselves are descriptive enough, so we
can also pass an anonymous function (a lambda term) to verify
that represents our statement.
In Imandra, we use fun
to create an anonymous function:
verify (fun x > f x <> 158)
 : Z.t > bool = <fun> module CX : sig val x : Z.t end
Counterexample (after 0 steps, 0.012s): let x : int = 69
ground_instances:  0  
definitions:  0  
inductions:  0  
search_time:  0.012s  
details:  Expand

start[0.012s] not ((if ( :var_0: ) > 99 then 100 else if (( :var_0: ) < 70) && (( :var_0: ) > 23) then 89 + ( :var_0: ) else if ( :var_0: ) > 20 then (if ( :var_0: ) > 22 then 9 else …) + 20 else if ( :var_0: ) > (2) then 103 else 99) = 158)
simplify
into: not ((( :var_0: ) <= 99) && ((if not (70 <= ( :var_0: )) && not (( :var_0: ) <= 23) then 89 + ( :var_0: ) else if ( :var_0: ) <= 20 then if ( :var_0: ) <= (2) then 99 else 103 else 20 + (if ( :var_0: ) <= 22 then … else 9)) = 158))
expansions: []
rewrite_steps: forward_chaining:  Sat (Some let x : int = (Z.of_nativeint (69n)) )
Imandra has found our statement to be false, and has also found us a concrete counterexample to demonstrate. Let's try executing f
with that value to confirm:
Imandra has derived for us that if x=69
, then f x
is equal to 158
, so the conjecture (fun x > f x <> 158)
is not true! Imandra has given us a concrete counterexample refuting this conjecture.
In Imandra, all counterexamples are "firstclass" values, and are automatically reflected into the runtime in a module (namespace) called CX
. So, another way to experiment with that counterexample is to utilise the CX
module that the verify
command constructed for us:
Region Decomposition¶
We can also ask Imandra to decompose our function to get a symbolic representation of its statespace. This decomposes the (potentially infinite) statespace into a finite number of symbolically described regions, each describing a class of behaviours of the function.
For each region it is proved that if the inputs of the function satisfy the constraints, then the output of the function satisfies the invariant. Furthermore, Imandra proves coverage: every possible concrete behaviour of the function is represented by a region in the decomposition:
Modular_decomp.top "f"
 : Modular_decomp_intf.decomp_ref = <abstr>
No group selected.
 Concrete regions are numbered
 Unnumbered regions are groups whose children share a particular constraint
 Click on a region to view its details
 Double click on a region to zoom in on it
 Shift+double click to zoom out
 Hit escape to reset back to the top
<constraint>
<invariant>
Reg_id  Constraints  Invariant 

6 
 100 
5 
 89 + x 
4 
 120 + x 
3 
 29 
2 
 103 
1 
 99 
0 
 29 
Click on the different full regions (those subdiagrams of the Voronoi diagram starting with R
) and inspect their constraints and invariant. Note that the invariant may depend on the input value (x
), e.g., in regions corresponding to branches of the function f
where it returns x
plus some constant.
Region decompositions form the basis of many powerful Imandra features, including forms of reachability analysis and automated testsuite generation and auditing.
Recursion and Induction¶
Imandra's reasoning power really shines in the analysis of recursive functions.
Let's define a simple recursive summation function, sum : int list > int
, and reason about it.
let rec sum x = match x with
 [] > 0
 x :: xs > x + sum xs
val sum : Z.t list > Z.t = <fun>
Termination proof
original:  sum x  
sub:  sum (List.tl x)  
original ordinal:  Ordinal.Int (_cnt x)  
sub ordinal:  Ordinal.Int (_cnt (List.tl x))  
path:  [x <> []]  
proof:  detailed proof
Expand

We can ask Imandra lots of interesting questions about our functions. For example, we can use Imandra's instance
command to ask Imandra to "solve" for inputs satisfying various constraints:
instance (fun x > List.length x >= 10 && sum x = List.length x + 17)
 : Z.t list > bool = <fun> module CX : sig val x : Z.t list end
Instance (after 22 steps, 0.020s): let x : int list = [(10620); 3583; 609; (1221); (10318); 1888; 5904; 5481; 2275; 2446]
ground_instances:  22  
definitions:  0  
inductions:  0  
search_time:  0.020s  
details:  Expand

start[0.020s] let (_x_0 : int) = List.length ( :var_0: ) in (_x_0 >= 10) && (sum ( :var_0: ) = _x_0 + 17)
simplify
into: let (_x_0 : int) = List.length ( :var_0: ) in (_x_0 >= 10) && (sum ( :var_0: ) = 17 + _x_0)
expansions: []
rewrite_steps: forward_chaining:  unroll
expr: (sum_1254/client x_1258/client)
expansions:  unroll
expr: (List.length_419/server x_1258/client)
expansions:  unroll
expr: (sum_1254/client (get.::.1_418/server x_1258/client))
expansions:  unroll
expr: (List.length_419/server (get.::.1_418/server x_1258/client))
expansions:  unroll
expr: (sum_1254/client (get.::.1_418/server (get.::.1_418/server x_1258/client)))
expansions:  unroll
expr: (List.length_419/server (get.::.1_418/server (get.::.1_418/server x_1258/client)))
expansions:  unroll
expr: (sum_1254/client (get.::.1_418/server (get.::.1_418/server (get.::.1_418/ser…
expansions:  unroll
expr: (List.length_419/server (get.::.1_418/server (get.::.1_418/server (get.::.1_418/server…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_418/server (get.::.1_418/server (get.::.1_418/…
expansions:  Sat (Some let x : int list = [(Z.of_nativeint (10620n)); (Z.of_nativeint (3583n)); (Z.of_nativeint (609n)); (Z.of_nativeint (1221n)); (Z.of_nativeint (10318n)); (Z.of_nativeint (1888n)); (Z.of_nativeint (5904n)); (Z.of_nativeint (5481n)); (Z.of_nativeint (2275n)); (Z.of_nativeint (2446n))] )
We can compute with this synthesized instance, as Imandra installs it in the CX
module:
Now, let's ask Imandra to prove a conjecture we have about sum
.
For example, is it always the case that sum x >= 0
?
verify (fun x > sum x >= 0)
 : Z.t list > bool = <fun> module CX : sig val x : Z.t list end
Counterexample (after 2 steps, 0.007s): let x : int list = [(1)]
ground_instances:  2  
definitions:  0  
inductions:  0  
search_time:  0.007s  
details:  Expand

start[0.007s] sum ( :var_0: ) >= 0
 unroll
expr: (sum_1254/client x_1260/client)
expansions:  unroll
expr: (sum_1254/client (get.::.1_454/server x_1260/client))
expansions:  Sat (Some let x : int list = [(Z.of_nativeint (1n))] )
Imandra tells us the (obvious) answer: This conjecture is false! Indeed, we can compute with the counterexample to see:
Ah, of course! How can we refine this conjecture to make it true? Well, we can add an additional hypothesis that every element of the list x
is nonnegative. Let's define a function psd
to express this:
let psd = List.for_all (fun x > x >= 0)
val psd : Z.t list > bool = <fun>
Now, let's ask Imandra to prove our improved conjecture:
verify (fun x > psd x ==> sum x >= 0)
 : Z.t list > bool = <fun>
expanded: 

blocked: 

ground_instances:  100 
definitions:  0 
inductions:  0 
search_time:  0.121s 
start[0.121s] List.for_all anon_fun.psd.1 ( :var_0: ) ==> sum ( :var_0: ) >= 0
simplify
into: not (List.for_all anon_fun.psd.1 ( :var_0: ))  (sum ( :var_0: ) >= 0)
expansions: []
rewrite_steps: forward_chaining:  unroll
expr: (sum_1254/client x_368/server)
expansions:  unroll
expr: (List.for_all_369/server x_368/server)
expansions:  unroll
expr: (sum_1254/client (get.::.1_367/server x_368/server))
expansions:  unroll
expr: (List.for_all_369/server (get.::.1_367/server x_368/server))
expansions:  unroll
expr: (sum_1254/client (get.::.1_367/server (get.::.1_367/server x_368/server)))
expansions:  unroll
expr: (List.for_all_369/server (get.::.1_367/server (get.::.1_367/server x_368/server)))
expansions:  unroll
expr: (sum_1254/client (get.::.1_367/server (get.::.1_367/server (get.::.1_367/ser…
expansions:  unroll
expr: (List.for_all_369/server (get.::.1_367/server (get.::.1_367/server (get.::.1_367/server…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:  unroll
expr: (let ((a!1 (get.::.1_367/server (get.::.1_367/server (get.::.1_367/…
expansions:
When we gave this fact to Imandra, it attempted to prove it using a form of bounded model checking. As it turns out, this type of reasoning is not sufficient for establishing this conjecture. However, Imandra tells us something very useful: that up to its current recursion unrolling bound of 100
, there exist no counterexamples to this conjecture.
For many practical problems, this type of bounded model checking establishing there exist no counterexamples up to depth k is sufficient. You may enjoy inspecting the call graph
of this bounded verification to understand the structure of Imandra's statespace exploration.
But, we can do even better. We'll ask Imandra to prove this fact for all possible cases. To do this, we'll ask Imandra to use induction. In fact, Imandra has a powerful [@@auto]
proof strategy which will apply induction automatically. Let's use it!
verify (fun x > psd x ==> sum x >= 0) [@@auto]
 : Z.t list > bool = <fun> Goal: psd x ==> sum x >= 0. 1 nontautological subgoal. Subgoal 1: H0. List.for_all anon_fun.psd.1 x  sum x >= 0 Must try induction. The recursive terms in the conjecture suggest 2 inductions. Subsumption and merging reduces this to 1. We shall induct according to a scheme derived from List.for_all. Induction scheme: (not (x <> []) ==> φ x) && (x <> [] && φ (List.tl x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: H0. List.for_all anon_fun.psd.1 x  C0. x <> [] C1. sum x >= 0 But simplification reduces this to true, using the definitions of List.for_all and sum. Subgoal 1.1: H0. x <> [] H1. List.for_all anon_fun.psd.1 (List.tl x) ==> sum (List.tl x) >= 0 H2. List.for_all anon_fun.psd.1 x  sum x >= 0 But simplification reduces this to true, using the definitions of List.for_all and sum. ⓘ Rules: (:def List.for_all) (:def sum) (:induct List.for_all)
ground_instances:  0 
definitions:  4 
inductions:  1 
search_time:  0.071s 
start[0.071s, "Goal"] List.for_all anon_fun.psd.1 ( :var_0: ) ==> sum ( :var_0: ) >= 0
subproof
not (List.for_all anon_fun.psd.1 x)  (sum x >= 0)start[0.071s, "1"] not (List.for_all anon_fun.psd.1 x)  (sum x >= 0)
induction on (functional ?) :scheme (not (x <> []) ==> φ x) && (x <> [] && φ (List.tl x) ==> φ x)
Split (let (_x_0 : bool) = x <> [] in let (_x_1 : bool) = sum x >= 0 in let (_x_2 : bool) = not (List.for_all anon_fun.psd.1 x) in let (_x_3 : int list) = List.tl x in (_x_0  _x_1  _x_2) && (not (_x_0 && (not (List.for_all anon_fun.psd.1 _x_3)  (sum _x_3 >= 0)))  _x_1  _x_2) :cases [not (List.for_all anon_fun.psd.1 x)  x <> []  (sum x >= 0); let (_x_0 : int list) = List.tl x in not (x <> [])  not (List.for_all anon_fun.psd.1 _x_0 ==> sum _x_0 >= 0)  not (List.for_all anon_fun.psd.1 x)  (sum x >= 0)])
subproof
let (_x_0 : int list) = List.tl x in not (x <> [])  not (List.for_all anon_fun.psd.1 _x_0 ==> sum _x_0 >= 0)  not (List.for_all anon_fun.psd.1 x)  (sum x >= 0)start[0.036s, "1.1"] let (_x_0 : int list) = List.tl x in not (x <> [])  not (List.for_all anon_fun.psd.1 _x_0 ==> sum _x_0 >= 0)  not (List.for_all anon_fun.psd.1 x)  (sum x >= 0)
simplify
into: true
expansions: [sum, List.for_all]
rewrite_steps: forward_chaining:
subproof
not (List.for_all anon_fun.psd.1 x)  x <> []  (sum x >= 0)start[0.036s, "1.2"] not (List.for_all anon_fun.psd.1 x)  x <> []  (sum x >= 0)
simplify
into: true
expansions: [sum, List.for_all]
rewrite_steps: forward_chaining:
Excellent. Imandra has proved this property for us for all possible inputs automatically by induction.
We hope you enjoyed this quick introduction!