ISoLA 2026 — Companion Artifact

The TLA+ Trifecta walks into a bar, the bartender ask Why3?

Ion Chirica, Mário Pereira, Jorge Sousa Pinto

This is the companion artifact page for the ISoLA 2026 paper “The TLA+ Trifecta walks into a bar, the bartender ask Why3?”. It provides access to the tools, repositories, and case studies used in the paper.

Proof results for both theories can be found on the proof artifacts page.

Repositories

Why3 Deductive program verification platform used throughout.
Why3-do WhyML library for state machine specifications and distributed systems.

Case Studies

The case studies below correspond to the examples discussed in the paper. Click view source on any entry to inspect the Why3 source.

ATD Asynchronous termination detection ▶ view source

module ATD

  use export int.Int
  use export set.Fset
  use export map.Map
  use export map.Const

  val constant n : int
    ensures { result > 0 }

  predicate is_node (i: int) = 0 <= i < n

  type world = {
    active : map int bool; (* Int -> Bool *)
    pending : map int int; (* Int -> Int *)
    termination_detected : bool;
  }

  predicate type_ok (s: world) = forall i. is_node i -> s.pending[i] >= 0

  predicate terminated (w: world) = forall i. is_node i -> (not w.active[i] /\ w.pending[i] = 0)

  predicate safe (w: world) = w.termination_detected -> terminated w

  predicate inv (w:world) = type_ok w /\ safe w

  inductive init world =
   | init : forall w. ((forall i. is_node i -> w.pending[i] = 0) /\ (w.termination_detected = false)) -> init w
   | init' : forall w. ((forall i. is_node i -> w.pending[i] = 0) /\ (w.termination_detected = terminated w)) -> init w

  let ghost predicate initWorld (w:world)
    ensures { result -> inv w }
  = init w 

  predicate receive_message_enabled (w: world) (i: int) = is_node i /\ w.pending[i] > 0
    
  let ghost function receive_message (w:world) (i: int) : world
    requires { receive_message_enabled w i }
    ensures  { inv w -> inv result }
  = { w with active = w.active[i <- true]; pending = w.pending[i <- w.pending[i] - 1] }

  predicate terminate_enabled (w: world) (i: int) = is_node i /\ w.active[i]

  let ghost function terminate_nd1 (w:world) (i: int) : world
    requires { terminate_enabled w i }
    ensures  { inv w -> inv result }
  =
    let w = { w with active = w.active[i <- false] } in
    { w with termination_detected = w.termination_detected; }

  let ghost function terminate_nd2 (w:world) (i: int) : world
    requires { terminate_enabled w i }
    ensures  { inv w -> inv result }
  =
    let w = { w with active = w.active[i <- false] } in
    { w with termination_detected = terminated w; }

  predicate send_message_enabled (w: world) (i j: int) = is_node i /\ is_node j /\ w.active[i]

  let ghost function send_message (w:world) (i j: int) : world
    requires { send_message_enabled w i j }
    ensures  { inv w -> inv result }
  = { w with pending = w.pending[j <- w.pending[j] + 1] }
  
  predicate detect_termination_enabled (w: world) = terminated w

  let ghost function detect_termination (w:world) : world
    requires { detect_termination_enabled w }
    ensures  { inv w -> inv result }
  = { w with termination_detected = true } 

  inductive stepind world world =
  | receive_message : forall w :world, i :int.
      receive_message_enabled w i ->
        stepind w (receive_message w i)

  | terminate_nd1 : forall w :world, i :int.
      terminate_enabled w i ->
        stepind w (terminate_nd1 w i)
  | terminate_nd2 : forall w :world, i :int.
      terminate_enabled w i ->
        stepind w (terminate_nd2 w i)

  | send_message : forall w :world, i :int, j: int.
      send_message_enabled w i j ->
        stepind w (send_message w i j)

  | detect_termination : forall w :world.
      detect_termination_enabled w ->
        stepind w (detect_termination w)

  let ghost predicate step (w1:world) (w2:world) = stepind w1 w2

  clone export inductiveness.Inductiveness with 
    type world, predicate inv, val initWorld, val step

end

Download .mlw Proof results

EWD998 Dijkstra’s termination detection algorithm ▶ view source

module EWD998

  use atd.ATD as ATD

  use export int.Int
  use export set.Fset
  use export map.Map
  use export map.MapSum
  use export map.Const

  constant n : int = ATD.n

  predicate is_node (i: int) = ATD.is_node i

  type color = White | Black
  type token = {
    pos     : int;
    q       : int;
    t_color : color
  } 
  
  type world = {
    active  : map int bool;  (* activation status of nodes *)
    color   : map int color; (* color of nodes *)
    counter : map int int;  (* number of sent messages *)
    pending : map int int;  (* number of messages in transit to node *)
    token   : token  (* token structure *)
  }

  let ghost function map_sum (m: map int int) (l u: int) =
      sum m l (u + 1)

  predicate termination_detected (w: world) =
     w.token.pos = 0 /\ w.token.t_color = White /\ w.token.q + w.counter[0] = 0 
   /\ w.color[0] = White /\ not w.active[0]

  let ghost function sum_B (w: world) = sum w.pending 0 n 

  let ghost function sum_Counter (w: world) = sum w.counter 0 n 

  let ghost function sum_Range (w: world) (l u: int) = map_sum w.counter l u

  predicate terminated' (w: world) =
    termination_detected w -> (forall i. is_node i -> not w.active[i] /\ sum_B w = 0)

  let ghost function refn (w:world) : ATD.world =
    { ATD.active = w.active; ATD.pending = w.pending;
      ATD.termination_detected = termination_detected w (* terminated' w *) }

  predicate type_ok (w: world) = (forall i. is_node i -> w.pending[i] >= 0) /\ is_node w.token.pos

  predicate safe (w: world) =
  (* P0: The number of counted messages at each node and the number of messages in transit is consistent. *)
  sum_B w = sum_Counter w /\
  (* At least one of P1, P2, P3, P4 must hold *)
  (
    (* P1: (Ai: t < i < N: machine nr.i is passive) /\ 
           (Si: t < i < N: ci.i) = q *)
    ((forall i. w.token.pos < i < n -> not w.active[i] (* machine nr.i is passive *)) /\
     (if w.token.pos = n - 1 
      then w.token.q = 0
      else w.token.q = sum_Range w (w.token.pos + 1) (n - 1)))
    \/ (* P2: (Si: 0 <= i <= t: c.i) + q > 0. *)
    ((sum_Range w 0 (w.token.pos)) + w.token.q > 0)
    \/ (* P3: Ei: 0 <= i <= t : machine nr.i is black. *)
    (exists i. is_node i /\ 0 <= i <= w.token.pos /\ w.color[i] = Black)
    \/ (* P4: The token is black. *)
    (w.token.t_color = Black)
  )

  lemma b0nomessagepending :
   forall w. type_ok w /\ sum_B w = 0 -> forall i. is_node i -> w.pending[i] = 0

  predicate inv (w:world) = type_ok w /\ safe w

  predicate initWorld_p (w:world) =
    (forall i. is_node i -> w.pending[i] = 0 /\ w.counter[i] = 0) /\
    (is_node w.token.pos /\ w.token.q = 0 /\ w.token.t_color = Black) 

  let ghost predicate initWorld (w:world)
    ensures { result -> inv w }
    ensures { result -> ATD.init (refn w) }
  = initWorld_p w

  (*---------------------------- System ----------------------------------------*)
  predicate initiate_probe_enabled (w: world) =
    w.token.pos = 0 /\
    (w.token.t_color = Black \/ w.color[0] = Black \/ w.counter[0] + w.token.q > 0)
    
  let ghost function initiate_probe (w:world) : world
    requires { initiate_probe_enabled w }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ ATD.step (refn w) (refn result) }
  =
    let token' = { pos = n - 1; q = 0; t_color = White } in
    let color' = w.color[0 <- White] in
    { w with token = token'; color = color' }

  predicate pass_token_enabled (w: world) (i: int) =
    is_node i /\ not w.active[i] /\ w.token.pos = i /\ is_node (w.token.pos - 1)
    
  let ghost function pass_token (w:world) (i: int) : world
    requires { pass_token_enabled w i }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ ATD.step (refn w) (refn result) }
  =
    let token' = { pos = w.token.pos - 1;
                   q = w.token.q + w.counter[i];
                   t_color = (* w.color[i] *) match w.color[i] with
                             | Black -> Black
                             | _ -> w.token.t_color end } in
    let color' = w.color[i <- White] in
    let w' = { w with token = token'; color = color' } in
    w'

  (*--------------------------- Environment ------------------------------------*)

  let lemma sum_update (m: map int int) (l u i v: int)
    requires { l <= i < u }
    ensures  { map_sum (m[i <- v]) l u = map_sum m l u - m[i] + v }
  =
    let m' = m[i <- v] in
    (* everything past i retains the same values *)
    assert { forall k. i + 1 <= k <= u -> m[k] = m'[k] };
    (* i.e. the sum is the same *)
    assert { map_sum m' (i + 1) u = map_sum m (i + 1) u }

  predicate send_message_enabled (w: world) (i: int) =
    is_node i /\ w.active[i] /\ (exists j. is_node j /\ i <> j)

  let ghost function send_message (w:world) (i: int) : world
    requires { send_message_enabled w i }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ ATD.step (refn w) (refn result) }
  =
    let j = any int in
    assume { is_node j /\ i <> j };
    let pending_j = w.pending[j] in
    let counter_i = w.counter[i] in
    let w' = { w with pending = w.pending[j <- pending_j + 1];
             counter = w.counter[i <- counter_i + 1] } in

    (* P0 *)
    assert { inv w -> sum_B w' = sum_Counter w' by
             sum w'.counter 0 n = (sum w.counter 0 n) + 1 /\
             sum w'.pending 0 n = (sum w.pending 0 n) + 1 };
    w' 

  predicate receive_message_enabled (w: world) (i: int) =
    is_node i /\ is_node w.token.pos /\ (* huh TODO *)
    (forall i. is_node i -> w.pending[i] > 0 /\ w.counter[i] > 0) /\
    w.token.q > 0 /\ w.pending[i] > 0

  let ghost function receive_message (w:world) (i: int) : world
    requires { receive_message_enabled w i }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ ATD.step (refn w) (refn result) }
  =
    let w' = { w with pending = w.pending[i <- w.pending[i] - 1];
             counter = w.counter[i <- w.counter[i] - 1];
             color = w.color[i <- Black];
             active = w.active[i <- true] } in

    assert { inv w -> sum_B w' = sum_Counter w' by
             sum w'.pending 0 n = (sum w.pending 0 n) - 1 /\
             sum w'.counter 0 n = (sum w.counter 0 n) - 1 };
    w'
  
  predicate deactivate_enabled (w: world) (i: int) =
    is_node i /\ w.active[i]

  let ghost function deactivate (w:world) (i: int) : world
      requires { deactivate_enabled w i }
      ensures  { inv w -> inv result }
      ensures  { inv w -> refn result = refn w \/ ATD.step (refn w) (refn result) }
    =
      let w' = { w with active = w.active[i <- false] } in 
      w'

  inductive system world world =
  | initiate_probe : forall w: world.                initiate_probe_enabled w -> system w (initiate_probe w)
  | pass_token     : forall w: world, i: int. i <> 0 -> pass_token_enabled  w i  -> system w (pass_token w i)

  inductive environment world world =
  | send_message    : forall w: world, i: int. is_node i -> send_message_enabled    w i -> environment w (send_message w i)
  | receive_message : forall w: world, i: int. is_node i -> receive_message_enabled w i -> environment w (receive_message w i)
  | deactivate      : forall w: world, i: int. is_node i -> deactivate_enabled      w i -> environment w (deactivate w i)

  inductive stepind world world =
  | system: forall w w'. system w w' -> stepind w w'
  | environment: forall w w': world. environment w w' -> stepind w w'

  let ghost predicate step (w1:world) (w2:world) = stepind w1 w2

  clone refinement.Refinement with 
    type worldC=world, type worldA=ATD.world, 
    val refn,
    predicate invC=inv, predicate invA=ATD.inv,
    val initWorldC=initWorld, val initWorldA=ATD.initWorld,
    val stepC=step, val stepA=ATD.step

end

Download .mlw Proof results

Refinement Module Why3-do refinement module ▶ view source

module Refinement

  (* Abstract and concrete configurations/states *)
  type worldA
  type worldC


  (* Refinement map *)
  val ghost function refn (worldC) : worldA


  (* Abstract and concrete invariant predicates *)
  predicate invA (w:worldA)
  predicate invC (w:worldC)


  (* Abstract and concrete initial state predicates *) 
  val ghost predicate initWorldA (w:worldA)
    ensures { result -> invA w }

  val ghost predicate initWorldC (w:worldC)
    ensures { result -> invC w }
    ensures { result -> initWorldA (refn w) }


  (* Abstract and concrete transition relations *) 
  val ghost predicate stepA (w1:worldA) (w2:worldA)
    ensures { result -> invA w1 -> invA w2 }

  val ghost predicate stepC (w1:worldC) (w2:worldC)
    ensures { result -> invC w1 -> invC w2 }
    ensures { result -> invC w1 -> refn w1 = refn w2
                                \/ stepA (refn w1) (refn w2) }


  (* Reachability -- abstract *)
  inductive stepA_TR worldA worldA =
  | baseA : forall w :worldA. stepA_TR w w
  | stepA : forall w w' w'' : worldA.
      stepA_TR w w' -> stepA w' w'' -> stepA_TR w w''

  lemma inv_manySteps_A :
    forall w w' :worldA. stepA_TR w w' -> invA w -> invA w'

  predicate reachableA (w:worldA) = 
    exists w0 :worldA. initWorldA w0 /\ stepA_TR w0 w

  lemma inv_reachable_A :
    forall w :worldA. reachableA w -> invA w


  (* Reachability -- concrete *)
  inductive stepC_TR worldC worldC =
  | baseC : forall w :worldC. stepC_TR w w
  | stepC : forall w w' w'' : worldC.
      stepC_TR w w' -> stepC w' w'' -> stepC_TR w w''

  lemma inv_manySteps_C :
    forall w w' :worldC. stepC_TR w w' -> invC w -> invC w'

  predicate reachableC (w:worldC) = 
    exists w0 :worldC. initWorldC w0 /\ stepC_TR w0 w

  lemma inv_reachable_C :
    forall w :worldC. reachableC w -> invC w


  (* Refinement lemmas *) 
  lemma manySteps_refinement : forall w w' :worldC.
    invC w -> stepC_TR w w' -> stepA_TR (refn w) (refn w')

  lemma reachable_refn : forall w :worldC.
    reachableC w -> reachableA (refn w)

  lemma invariance_refn : forall w :worldC. reachableC w -> invA (refn w)

end

Download .mlw

Inductiveness Module Why3-do inductiveness module ▶ view source

module Inductiveness

  type world

  (*  invariant predicate *)
  predicate inv (w:world)

  (* state machine - initial states 
     and transition relation *)
  val ghost predicate initWorld (w:world) 
    ensures { result -> inv w }

  val ghost predicate step (w1:world) (w2:world)
    ensures { result -> inv w1 -> inv w2 }


  (* Reachable states *)
  inductive step_TR world world =
  | base : forall w :world. step_TR w w
  | step : forall w w' w'' : world.
      step_TR w w' -> step w' w'' -> step_TR w w''

  (* requires predicate induction *)
  lemma inv_manySteps :
    forall w w' :world. step_TR w w' -> inv w -> inv w'

  predicate reachable (w:world) =
    exists w0 :world. initWorld w0 /\ step_TR w0 w

  (* inductive invariants are invariant *)
  lemma inv_reachable :
    forall w :world. reachable w -> inv w

end

Download .mlw