Using Why3 for software verification

By default the input language is ML-based, called WhyML (.mlw extension). It's very beautiful language, but other languages are also supported:

• micro-C
• micro-Python (Python 3 subset)
• MLCFG
• Coma

See more about input languages.

Why3 has a lot of features. Lets group them:

VST / Rocq is very mature and solid here - low-level C is it's home. It was used for verification of SHA-256, HMAC, mbedTLS HMAC-DRBG, TweetNaCl / Curve25519 cryptography, garbage collection, graph algorithms, concurrent messaging, an HTTP key-value server, differential-equation solvers, and Reed--Solomon coding, etc. Canonical VST case study is verification of OpenSSL HMAC + SHA-256. The work also connected the C-level proof to CompCert's verified compilation to assembly. The authors describe it as combining source-program correctness, compiler correctness, and cryptographic-security proofs without gaps at the specification interfaces. Additionally to cryptography VST is widely used in memory work verification, it supports:

• pointers
• aliasing
• ownership
• memory invariants
• low-level data structures
• allocators
• and so on...

Also it is used for numerical scientific C, a lot of examples, network programming verification

See more about VST.

F* has an unusually strong real-world systems/security track record, arguably more concentrated around cryptography, networking, and verified low-level code than VST's.

The important distinction is that many of the projects below are part of the broader Project Everest ecosystem: F* is the specification/proof language, while tools such as KaRaMeL and Vale connect the proofs to C and assembly. Famous project where the code was verified and extracted is HACL*:

HACL* is a collection of verified cryptographic primitives implemented in F*, with extraction to C. It includes algorithms such as:

• Curve25519
• Ed25519
• AES
• SHA-2
• ChaCha20
• Poly1305
• various hash/MAC constructions

It was extracted to C and has been integrated into real software including Firefox, Linux, and WireGuard. Another project created with F* is EverCrypt:

EverCrypt is a larger cryptographic provider built on the Everest verification technology. It combines verified implementations of cryptographic primitives with:

• algorithm agility,
• hardware acceleration,
• architecture-specific implementations,
• runtime selection,
• CONSTANT-TIME GUARANTEES!

Another project: Vale (verified cryptographic assembly). Vale is designed specifically for verifying low-level assembly. It has been used to verify optimized cryptographic implementations, including assembly for:

• AES-GCM
• ChaCha20
• Poly1305
• Curve25519-related operations
• other cryptographic primitives

Vale supports x86/x64 and ARM-family architectures, and its verification is integrated with F* and Dafny.

Low*/Pulse was designed to give F* programs a C-like computational model:

• mutable buffers
• pointers
• arrays
• structs
• machine integers
• stack/heap memory
• explicit effects
• memory safety.

KaRaMeL then translates verified Low* programs into C.

VST scenario:

   existing C
       |
       v
VST separation logic
       |
       v
     proof
       |
       v
   CompCert
       |
       v
  machine code

F* scenario:

         specification
               |
               v
               F*
               |
               v
low-level verified implementation
               |
          .----+-----.
          |          |
          C         ASM
          |          |
        KaRaMeL    Vale

VST asks:

"How can I prove this C program?"

F* often asks:

"How can I construct an implementation whose relationship to the specification is machine-checked, and then extract it to C or connect it to verified assembly?"

For learning formal verification itself, I'd start with Dafny.

For learning automated deductive verification, Dafny or Why3.

For verified systems/security programming, F*.

For deep C/pointer/separation-logic verification, VST/Rocq.

And if your eventual goal is specifically C + handwritten x86-64/ARM assembly, I'd spend the learning effort on F + Vale* or VST/CompCert + Vale, rather than trying to make Dafny or Why3 do all of it.

Dafny - very simple. Why3 more complex but not too much. F* - yes, more complex even. Rocq/VST - absolute "hardcore", by AI they look as:

set -o pipefail
[ -z "$1" ] && { echo 'Arg1: path to .mlw file' ; exit 1; }
[ "${WHY3_SPLITVC+x}" ] && split_opt='-a split_vc'
why3 prove -P ${WHY3_PROVER:-z3} -t ${WHY3_TIMEOUT:-10} "$1" $split_opt $WHY3_OPTS | tee _"$1".proven
echo '-----------------------------------------------------'
grep -P -B 2 '^Prover result is: (?!Valid)' _"$1".proven | tee _"$1".error
[ $? -eq 0 ] && { echo; echo '*** ERROR: NOT PROVEN! ***'; exit 1; } || exit 0

Example of call:

$ WHY3_SPLITVC= sh prove.sh Test1.mlw

SAT solves boolean "satisfiability" answering the question: "Can I assign true/false to these boolean variables so that the whole formula becomes true?", example:

Input formula :            (A OR B) AND (NOT A OR C)

A SAT solver might find :  A = false
                           B = true
                           C = false

                           

It's kind of utility helper in the world of automatic logic. SAT works fundamentally with true/false, AND, OR, NOT... It is something like "constraint programming over boolean domain".

A SAT solver doesn't inherently understand things like:

x + 1 > x

because x there isn't a boolean variable.

SMT means "Satisfiability Modulo Theories", it answers the question: "Is there an assignment that makes this formula true?", but SMT allows variables from particular mathematical theories.

For example, integer arithmetic:

Input :                   x: Int
                          y: Int
                          x > 10
                          y = x + 5
                          y < 20

                          
SMT solver might find :   x = 11
                          y = 16

SMT works in domains:

• integers and real numbers
• arithmetic
• arrays
• bit-vectors
• equality
• uninterpreted functions
• sometimes strings (CVC 4 (strings), etc), floating point, etc.

Modern SMT solvers combine: Boolean reasoning of SAT with its own standard Theory reasoning, i.e., SAT today is usually embedded part of SMT.

Why3, Dafny, F*, etc, delegate "simple" work to SMT. Rocq, LEAN - do not (they can do all work by self, but they allow to use external solvers).

                .---------------------.
                |       WhyML         ‖
                |  program + specs    ‖
                `======================
                           |
             verification  |              
                           v
                .---------------------.
                |   Why3 VC Generator ‖
                |       (VCgen)       ‖
                `======================
                           |
                      Verification
                    Conditions (VCs)
                           |
                           v
                .---------------------.
                |   Why3 Transform    ‖
                |                     ‖
                | simplify / split /  ‖
                | instantiate / etc.  ‖
                `======================
                           |
                SMT-LIB    |         
               .-----------+-----------.
               |           |           |
               v           v           v
            .-----.     .-----.     .------.
  SMT       | Z3  ‖     |CVC5 ‖     | Alt- ‖
solvers     |     ‖     |     ‖     | Ergo ‖
            `======     `======     `=======
               |           |           |
               `-----------+-----------'
                           |
                       SAT, UNSAT
                           |
                           v
                .---------------------.
                |        Why3         ‖
                |    proof result     ‖
                `======================

The "route" of the input WhyML program;

.----------[ WhyML ]-----------.
|  let f (x: int) : int        ‖    Your WhyML code
|   ensures { result >= x } =  ‖   
|  x + 1                       ‖   
`===============================   
               |                   Why3 generates VC
               v                   (verification condition)
 .----------[ VC ]-------------.   
 |     ∀ x:int. x + 1 >= x     ‖   
 `==============================   Why3 translates it to the language
               |                   understood by the selected prover
               v                   (typically SMT-LIB)
.---------[ Z3 QUERY ]----------.  
| (declare-const x Int)         ‖  
| (assert (not (>= (+ x 1) x))) ‖  
| (check-sat)                   ‖  
`================================   Why3 gets output from SMT solver...

Why3 is not a frontend to a SMT solver - Why3 has its own intermediate logical language and transformation system. It can manipulate a proof goal before handing it to an automated prover:

             WhyML
               |
               v
         .------------.   ....
         |   VCgen    ‖       ⋱
         `=============        :
              VC               :
               |               :
               v               :
         .------------.         ⋱  Why3
         | Transform  ‖         ⋰  work
         |            ‖        :
         | split_goal ‖        :
         | simplify   ‖        :
         | induction  ‖        :
         | specialize ‖        :
         `=============   ....⋰
               |
      .--------+--------.
      v                 v
  SMT solver       Interactive
  (Z3/CVC5/...)      prover

Also Why3 can combine provers:

         :
        VC
         |
    .----+----.
    v         v
   Z3      Alt-Ergo
    |         |
    `----+----'
         |
         v
       proved

Also Why3 records the resulting proof information so that the verification can be checked/replayed later.

1   type num =
2     | NaN
3     | MinusInf
4     | Fin int
5     | PlusInf

Here we declare ADT which models Not-a-Number, Minus Infinity, Finite integer (usual), Plus Infinity. We use it later, in the original Python code I used float numbers and Python support these special values internally.

 1   let calc_diffs (ps: array int) (absolute: bool) : array int =
 2   ensures {
 3     (length ps = 0 -> length result = 0) /\
 4     (length ps > 0 -> length result = length ps - 1)
 5   }
 6     let diffs_num = max ((length ps) - 1) 0 in
 7     let diffs = make diffs_num 0 in
 8     let i:ref int = ref 0 in
 9     if diffs_num = 0 then
10       diffs
11     else begin
12       while !i <> length ps - 1 do
13       invariant { 0 <= !i <= length ps - 1 }
14       invariant { !i <= length diffs }
15       variant { length ps - 1 - !i }
16         let diff = ps[!i + 1] - ps[!i] in
17         let diff = if absolute then abs diff else diff in
18         diffs[!i] <- diff;
19         incr i
20       done;
21       diffs
22     end

First, we see on 1 the declaration of the function calc_diffs which has 2 arguments: an array of integers and a boolean, and it returns an array of integers. Also it has one postcondition on line 2 (see ensures {..}), it could have preconditions too...

postcondition on 2 says: there are 2 statements - they are formed as first AND second ("and" is /\):

1. (length ps = 0 -> length result = 0) If the length of the argument ps is 0 then the result of the function will have a length 0 too
2. (length ps > 0 -> length result = length ps - 1) If the argument ps is not empty then the length of the result is lesser of ps by 1.

Why3 will check the code of the function and will prove or refute such statements, you can do it by self:

1. initially the loop variable i is 0
2. it's bound is length ps - 1 (on 12)

Why3 does it automatically, for you.

These properties (postconditions in the case) are important: you know what to expect from the function.

Also they will be used in proving of other pieces of the code, they are "a contract", and when it is called somewhere, Why3 can reason about its result.

Types matter - they are also controlled by Why3 - if an expression violates the declared type, it is also reported as an error, obviously.

Inside while loop we see invariant and variant expressions. "Invariant" describes something that does not change - it is checked too also this knowledge is remembered as a fact and can be used later for further proving. These 2 invariant expressions do state:

• invariant { 0 <= !i <= length ps - 1 } we guarantee inside the loop that i is always in this diapason, i.e., [0..length ps-1]
• invariant { !i <= length diffs } also we guarantee that i is always lesser or equal to the length of the array diffs

Invariants also can help proving of other claims - without them some claims will not be proven.

Little note: ! in the front of i is "dereferencing" like "*" in C - "take the content of the reference" - to be mutable we declared i as reference.

OK, also we see "variant". The idea of a variant expression is more interesting: it guarantees that something is "decreasing" - it states "what" does it. Why do we need it? Usually it is needed in:

• while-loop (in for-loop it is obvious, so it is redundant and syntactically denied)
• in recursive functions

"Variants" state that something becomes smaller and smaller and this thing is known as something having "ZERO" - the smallest form, it cannot become "smaller" and it guarantees Why3 that looping construction will complete (it is not forever-running, it will terminate) - most looping constructions are such ones. Sure, exceptions of this are supported (diverges keyword). OK, so here: variant { length ps - 1 - !i } we say that this "thing" (expression) becomes smaller and smaller, considering the length of ps is 3:

Theorem provers know: if we hit the smallest "thing" (and it checks the code sure, that it's true), then we reach the end of the looping. It means - no infinite loop here.

Variant expression just focus Why3 what "thing" to check for termination - the decrease of it is checked by Why3 itself

Such "things" can be integers, lists (reaching of Nil - the empty tail), etc.

And these "variants" and "invariants" give knowledge about looping constructions: what is true on every step/iteration, what does guarantee that the end of the loop or recursion.

Let's continue.

 1   let rec list_min (l: L.list int) : int =
 2   requires { l <> L.Nil }
 3   variant  { LL.length l }
 4     match l with
 5     | L.Nil -> absurd
 6     | L.Cons x L.Nil -> x
 7     | L.Cons x r ->
 8         let m = list_min r in
 9         if x < m then x else m
10     end

New here is that it consumes list, not array. Also it is a "program" (i.e, computational) function (due to let keyword!). And it is recursive (rec keyword). It has requires expression which says that list_min is allowed to be called only with a non-empty list: Why3 will check all places where it is called. Also it is a contract meaning: a function will guarantee (see ensures) if its requirements will be satisfied.

And you see variant again focusing Why3 what should be checked for termination - it is the length of the list l, also we can write directly variant { l } - it is the same. It is our termination measure, because we call list_min recursively passing it the tail of the list l, which means that on every call l becomes smaller and smaller (we "chop" the list). Can we violate the requirement? No, because we stop on line 6 and return x without to dive deeper in a recursive call. Also we have pattern matching on l and it should have a branch for empty list - it is line 5. What do we do there? We use absurd which means in the context of computational/program code - "check if it is really absurd code and it can never happen". Why3 will check it (in computational context). If it is not - it will be reported as an error!

This is helper-function, needed mostly in logic (so, I could make it ghost, I think):

  let rec function list_nth (l: L.list int) (n: int): option int =
  requires { 0 <= n < LL.length l }
  ensures {
    match result with
    | Some el -> LM.mem el l
    | None    -> false
    end
  }
  variant { n }
  match l with
  | L.Cons x tl -> if n = 0 then Some x else list_nth tl (n - 1)
  | L.Nil -> None
  end

How to read it: input argument n must be in this range being passed to the function (it reminds refinement types) and cos it's a recursive function - it have a "measure of termination", i.e., variant expression in its contract: we recursively call ourselves (rec) with decreasing of n. More interesting is ensures part of the contract: it guarantees that the result exists if it is a member (see mem) of the list l. It sounds strange, but I used it to expose out the connection between "nth item" and "it is an item of list". It sounds strange but provers often need facts obvious to you but not for them.

I checked Python program where lists have some duality: they are easy accessible by an index but at the same time they are like usual lists: you can append items to them, etc. So, I used arrays and lists in my WhyML - and I feel that it is not the best solution :)

Anyway, so, I needed a way to convert list to array. This helper function does it. It ensures not only preserving of the length but also that the same elements are on the same positions - see the second ensures on line 3:

 1  let list_to_array (l: L.list int) : array int =
 2    ensures { LL.length l = length result }
 3    ensures {
 4      (* preserving of elements *)
 5      forall k:int. 0 <= k < LL.length l ->
 6        Some result[k] = list_nth l k
 7    }
 8    let a = make (LL.length l) 0 in
 9    for i = 0 to LL.length l - 1 do
10      invariant { 0 <= i <= LL.length l }
11      invariant {
12        forall k:int. 0 <= k < i ->
13          Some a[k] = list_nth l k      (* check of history *)
14      }
15      match list_nth l i with
16      | Some el -> a[i] <- el;
17      | None    -> absurd
18      end;
19    done;
20    a

Invariants are needed to say: "At every loop iteration, the current state must satisfy this formula, and this formula summarizes the relevant consequences of all previous iterations.", it is like setting of the induction hypothesis like:

∀ k < i →
    a[k] = l[k]

roughly, we can use why3 command's option --print-theory:

   ...
 1   (forall a1:array int.
 2     a1.length = a.length ->
 3     (forall i:int.                   ⋱... our  for i = 0 to LL.length l - 1
 4       (0 <= i /\ i <= o2) /\         ⋰
 5       (0 <= i /\ i <= length1 l) /\                                    ⋱... invariants
 6       (forall k:int. 0 <= k /\ k < i -> Some a1[k] = list_nth l k) ->  ⋰
 7       (0 <= i /\ i < length1 l) /\
 8       (let o3 = list_nth l i in
 9        match o3 with
10        | Some el -> mem el l
11        | None -> false
12        end ->
   ...
22           (0 <= (i + 1) /\ (i + 1) <= length1 l) &&
23        (forall k:int.
24          0 <= k /\ k < (i + 1) -> Some a2[k] = list_nth l k))
   ...

Something like:

    Assume invariant(i)
            |
            v
    execute iteration
            |
            v
  prove invariant(i+1)

This converts an unbounded history problem into a finite induction proof: "Every iteration I've performed so far correctly copied its element." It reminds the usual induction:

Base:
    I(S₀, 0)

Step:
    I(Sᵢ, i) ∧ transition(Sᵢ, Sᵢ₊₁)
       ⇒ I(Sᵢ₊₁, i+1)

Exit:
    I(Sₙ, n) ∧ exit-condition
       ⇒ postcondition

where S is for "a state".

Another helper ghost (see predicate) code:

1   predicate list_elems_are_correct_index (l: L.list int) (n: int) =
2   (* The predicate checks that all elements in the list `l` can be index bounded by `n`,
3    * ie, 0 <= el < n. It is used in `list_elems_are_correct_index__append_singleton` lemma
4    *)
5     match l with
6     | L.Nil      -> true
7     | L.Cons x r -> 0 <= x < n /\ list_elems_are_correct_index r n
8     end

It checks that all items in a list can be indexes of some sized object which size is n, i.e., they are bound by [0..n). Then - lemma, it is helper-theorem - something that will be proven and later used in other proofs.

 1   (* This lemma is needed to prove the invariant:
 2    *
 3    *   invariant { list_elems_are_correct_index !res_ranges (length res_ps_arr) }
 4    *
 5    * in `approximate_by_rectangles`. This invariant tells that every item is `res_ranges`
 6    * is a index of items in `res_ps`/`res_ps_arr` (`res_ranges` is a list of indexes, so
 7    * no one item in `res_ranges` can violate the `res_ps` bounds - it can be useful in
 8    * the next function: `find_clusters_centers`). But to prove this invarint, we have
 9    * to hint Why3 with some lemma. Without it, we hit timeout/out of memory.
10    *
11    * It seems the timeout problem is connected with construction of a list and need to
12    * check the invariant when the list is growing (?) - we add `i` to the list, and we
13    * know that `i` is inside bounds, so Why3 has to check that adding only of `i` to a
14    * list means that all items of that list are inside the same bounds. More detailed:
15    * Z3/CVC4/... do not automatically know that `list_elems_lt` is preserved by `++` !
16    *
17    * This lemma proves it by induction. `requires` is A, `ensures` is B in A -> B.
18    * `variant` is a termination measure (bcs the lemma is recursive).
19    * The logic of the lemma is in its body (it is like FStar) - returning of () means
20    * "true/fact!", and we prove the base of the induction for an empty list then
21    * we state that for non-empty list we pass through it to the base case ("next step"?),
22    * the proposition that we prove is B, ie:
23    *
24    *   ∀x: 0 <= x < n                             (any integer that is also valid index)
25    *   list_elems_are_correct_index (l ++ [x]) n  (property is preserved after .. ++ [x])
26    * 
27    *)
28   let rec lemma list_elems_are_correct_index__append_singleton (l: L.list int) (x n: int) =
29   requires { list_elems_are_correct_index l n /\ 0 <= x < n }
30   variant { LL.length l }
31   ensures { list_elems_are_correct_index (l ++ L.Cons x L.Nil) n }
32     match l with
33     | L.Nil      -> ()
34     | L.Cons _ r -> list_elems_are_correct_index__append_singleton r x n
35     end

The idea of the lemma is that instead of asking the solver to discover that appending a VALID singleton preserves the property while reasoning about a growing list, the program can call the lemma and use its postcondition. Look:

requires:                              
    P(r) /\ Q

ensures:
    P(r ++ [x])

  I n d u c t i o n :
    
P([])                  -- base
P(y::r) -> P(r)        -- obtain ind. hypothesis (IH)
IH                     -- recursively prove tail
--------------
P(y::r)

What does L.Nil -> () mean in the lemma? It means:

1. There is no any PROGRAM operation to perform (it's let lemma)
2. Just verify that the contract follows from the current logical context (i.e., preconditions, postcondition)

Lets simplify them:

 1   predicate P (l) (n) =
 2     match l with
 3     | Nil -> true
 4     | Cons x r -> 0 <= x < n /\ P r n
 5     end
 6   
 7   let rec lemma foo (l) (x) (n) =
 8     requires { P l n /\ 0 <= x < n }
 9     variant { length l }
10     ensures { P (l ++ [x]) n }
11   
12     match l with
13     | Nil -> ()
14     | Cons _ r -> foo r x n
15     end

 1    (* This axiom is workaround for:
 2     *   let isovalue: int = isovalues_arr[ranges_arr[irange]] in
 3     * in `find_clusters_centers`, so Why3 be able to prove bounds violation, it has all info
 4     * for it but it cannot connect separate items (to connect list/array items bound by
 5     * `LL.length isovalues`, ie, `ranges/ranges_arr` values are 0..|isovalues|-1).
 6     *)
 7    
 8    axiom list_element_is_valid:
 9      forall l:L.list int, n k:int.
10        list_elems_are_correct_index l n ->
11        0 <= k < LL.length l ->
12        match list_nth l k with
13        | Some x -> 0 <= x < n
14        | None -> false
15        end

In short, if list_elems_are_correct_index l n, then it means that every item of l (indexed by k ∈ 0..|l|) is bounded too. I entered it as an axiom (it is just trusted, without to be provev), because I had problems with a proof of this obvious fact, yep. But this axiom helps to check bounds violations in let isovalue: int = isovalues_arr[ranges_arr[irange]]... later. Yes, Why3 performs bounds checking too.

 1   let approximate_by_rectangles (ps: array int)
 2                                 (tolerance: int) : (L.list int, L.list int) =
 3   requires { tolerance > 0 }
 4   (* invariants and asserts help to prove `ensures`, else they fail with timeout *)
 5   ensures {
 6     length ps > 0 ->
 7       match result with
 8       | (a, b) -> LL.length a > 0 /\ LL.length b > 0
 9       end
10   }
11   ensures {
12     match result with
13     | (a, b) -> LL.length a <= LL.length b
14     end  
15   }
16   ensures {
17     (* connects 1st,2nd items of the returning tuple: `a` is a list
18        of indexes in `b` *)
19     match result with
20     | (a, b) -> list_elems_are_correct_index a (LL.length b)
21     end
22   }
23     let res_ps: ref (L.list int) = ref L.Nil in
24     let res_ranges: ref (L.list int) = ref L.Nil in
25     let slice: ref (L.list int) = ref L.Nil in
26     for i = 0 to length ps - 1 do
27     invariant { 0 <= i <= length ps }
28     invariant { i > 0 -> LL.length !slice > 0 }
29     (* call of `list_to_array` in loop is horrible performance, but for proving - it
30      * is not not a problem. It is needed due to duality of Python's list (it is
31      * translation from Python) - it is indexable but also appendable/extendable *)
32       let p = ps[i] in
33       if LL.length !slice = 0 then
34         slice := !slice ++ (L.Cons p L.Nil)
35       else if new_rect_is_needed (list_to_array !slice) p tolerance then
36         begin
37           let slice_avg = calc_avg (list_to_array !slice) in
38           res_ps := !res_ps ++ (make_list (LL.length !slice) slice_avg);
39           slice := make_list 1 p
40         end
41       else
42         slice := !slice ++ (L.Cons p L.Nil)
43     done;
44     if LL.length !slice > 0 then
45       begin
46         let slice_avg = calc_avg (list_to_array !slice) in
47         res_ps := !res_ps ++ (make_list (LL.length !slice) slice_avg)
48       end;
49     assert { LL.length !slice > 0 -> LL.length !res_ps > 0 };
50     let pr: ref (option int) = ref None in
51     let res_ps_arr: array int = list_to_array !res_ps in
52     assert { length res_ps_arr = LL.length !res_ps };
53     for i = 0 to length res_ps_arr - 1 do
54     invariant { 0 <= i <= length res_ps_arr }
55     invariant { i > 0 -> LL.length !res_ranges > 0 }
56     invariant { LL.length !res_ranges <= i }  (* this is needed to avoid timeout on 2nd
57                                                * `ensures` of the function *)
58     invariant { list_elems_are_correct_index !res_ranges (length res_ps_arr) }
59       if i = 0 then
60         res_ranges := !res_ranges ++ (L.Cons i L.Nil)
61       else if not option_eq !pr (Some res_ps_arr[i]) then
62         res_ranges := !res_ranges ++ (L.Cons i L.Nil);
63       pr := Some res_ps_arr[i]
64     done;
65     assert { length ps > 0 -> (LL.length !res_ranges > 0) /\ (LL.length !res_ps > 0) };
66     (!res_ranges, !res_ps)

This function contains interesting postconditions about resulting 2 lists (combined in a tuple):

• for non-empty input array, both result lists are not empty
• the second result list is never smaller than the first one
• the first list contains only indexes of the second list

Also this fragment contains already known invariants (in for), pay attention, for does not use variants because it's naturally limited and asserts. Asserts must end with ";". Asserts:

• are proved
• are saved as facts in the logical context
• help to prove some other claims (as well as invariants help too)
• are kind of DOCUMENTATION about the code

  let find_clusters_centers
    (ranges isovalues: L.list int) (ratio: int) (nesting: int): L.list (int, int) =
  requires { LL.length ranges <= LL.length isovalues }
  requires { list_elems_are_correct_index ranges (LL.length isovalues) }
  if LL.length ranges = 0 || LL.length isovalues = 0 then
    L.Nil
  else begin
    let res: ref (L.list (int, int)) = ref L.Nil in
    let max_irange: int = LL.length ranges - 1 in
    let prev_isovalue: ref (option int) = ref None in
    let ranges_arr: array int = list_to_array ranges in
    let isovalues_arr: array int = list_to_array isovalues in
    for irange = 0 to max_irange do
      let isovalue: int = isovalues_arr[ranges_arr[irange]] in
      let skip_common: ref bool = ref false in
      let left: ref int = ref 0 in
      let right: ref int = ref 0 in    
      match !prev_isovalue with
      | None                 -> ()
      | Some prev_isovalue_v ->
        if isovalue > prev_isovalue_v &&
           num_ge (calc_ratio isovalue prev_isovalue_v) (Fin ratio) then
        begin
          right := ranges_arr[irange];
          left := ranges_arr[max (irange - 1) 0]
        end
        else if isovalue < prev_isovalue_v &&
                num_ge (calc_ratio prev_isovalue_v isovalue) (Fin ratio) then
        begin
          left := ranges_arr[irange];
          right := ranges_arr[min (irange + 1) max_irange]
        end
        else
        begin
          prev_isovalue := Some isovalue;
          skip_common := true
        end;
        if not !skip_common then
        begin
          if !right = !left then incr right;
          left := !left + nesting;
          right := !right + nesting;
          if LL.length !res = 0 ||
             not (option_tuple_eq (list_last !res) (Some (!left, !right))) then
            res := !res ++ (L.Cons (!left, !right) L.Nil);
        end
      end;
      prev_isovalue := Some isovalue
    done;
    !res
  end

Why3 checks bounds violation in: let isovalue: int = isovalues_arr[ranges_arr[irange]]. But to do it, it needs help (that lemma list_elems_are_correct_index__append_singleton but mostly the axiom-workaround!): all indexes are checked! Also we added it to the precondition:

  requires { list_elems_are_correct_index ranges (LL.length isovalues) }

This is complex bounds check because it should check that all items in ranges_arr array do not violate [0..|isovalues_arr|). Also Why3 checks that irange is in 0..|ranges_arr|.