TLA+ and Alloy are lower barrier to entry software verification tools. They are typically used on systems or protocol level models rather than modelling the exact source. There are many bugs that can appear at this level and they are super useful for clarifying your thinking.

CBMC is a tool I’m pretty bullish on. It is a bounded model checker for C code. It more or less unrolls all loops in normal compileable C to some depth and then throws that into a SAT or SMT solver.

What really makes this great is that there is no new language for software engineers to learn or accept. C has already made it in. People accept C as a useful pragmatic language. I found this a fascinating read in terms of how to make formal methods useable in industry Code-level model checking in the software development workflow at Amazon Web Services

Ultimately, there is surprisingly little difference between ordinary programming and a logic if you are trying to see the similarities. A logical spec is not that different writing a programmatic check. CBMC takes it’s specs largely in the form of regular asserts.

I think these advantages of CBMC are also useful even if you aren’t trying to prove things about C code. For all our bellyaching about C undefined behavior and so on, if you stick to a boring subset of the language and avoid pointers, it is a reasonable “Imp”. I kind of think is more structured or typed than TLA+ is in it’s design.

So I think it’s interesting to consider using C via CBMC for tasks that you might normally use TLA+ for. You get all sorts of tooling, training, and idioms for free.

Instead of writing a logical specification of the allowable transitions, you write a simulator. Instead of writing a logical specification of bad behavior, throw in some asserts. These are very obvious and reasonable things from an engineering perspective.

This simulator is by default executable / compileable and in fact swiftly executable since C is a fast language. This enables the options of fuzzing if you don’t want to use CBMC.

Follow along on colab https://colab.research.google.com/github/philzook58/philzook58.github.io/blob/master/pynb/2024-10-07-high_cbmc.ipynb

Die Hard

This is a collection of TLA+ examples https://github.com/tlaplus/Examples

One example is a water puzzle from Die Hard 3. https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla

%%file /tmp/DieHarder.tla

------------------------------ MODULE DieHard ------------------------------- 
(***************************************************************************)
(* In the movie Die Hard 3, the heroes must obtain exactly 4 gallons of     *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet.  Our    *)
(* goal: to get TLC to solve the problem for us.                           *)
(*                                                                         *)
(* First, we write a spec that describes all allowable behaviors of our    *)
(* heroes.                                                                  *)
(***************************************************************************)
EXTENDS Naturals
  (*************************************************************************)
  (* This statement imports the definitions of the ordinary operators on   *)
  (* natural numbers, such as +.                                           *)
  (*************************************************************************)
  
(***************************************************************************)
(* We next declare the specification's variables.                          *)
(***************************************************************************)
VARIABLES big,   \* The number of gallons of water in the 5 gallon jug.
          small  \* The number of gallons of water in the 3 gallon jug.


(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set.  A type          *)
(* invariant like this is not part of the specification, but it's          *)
(* generally a good idea to include it because it helps the reader         *)
(* understand the spec.  Moreover, having TLC check that it is an          *)
(* invariant of the spec catches errors that, in a typed language, are     *)
(* caught by type checking.                                                *)
(*                                                                         *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\   *)
(* or \/ denotes the conjunction or disjunction of those formulas.         *)
(* Indentation of subitems is significant, allowing one to eliminate lots  *)
(* of parentheses.  This makes a large formula much easier to read.        *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3 
          /\ big   \in 0..5


(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial      *)
(* values of the variables.  I like to name this predicate Init, but the   *)
(* name doesn't matter.                                                    *)
(***************************************************************************)
Init == /\ big = 0 
        /\ small = 0

(***************************************************************************)
(* Now we define the actions that our hero can perform.  There are three   *)
(* things they can do:                                                     *)
(*                                                                         *)
(*   - Pour water from the faucet into a jug.                              *)
(*                                                                         *)
(*   - Pour water from a jug onto the ground.                              *)
(*                                                                         *)
(*   - Pour water from one jug into another                                *)
(*                                                                         *)
(* We now consider the first two.  Since the jugs are not calibrated,      *)
(* partially filling or partially emptying a jug accomplishes nothing.     *)
(* So, the first two possibilities yield the following four possible       *)
(* actions.                                                                *)
(***************************************************************************)
FillSmallJug  == /\ small' = 3 
                 /\ big' = big

FillBigJug    == /\ big' = 5 
                 /\ small' = small

EmptySmallJug == /\ small' = 0 
                 /\ big' = big

EmptyBigJug   == /\ big' = 0 
                 /\ small' = small

(***************************************************************************)
(* We now consider pouring water from one jug into another.  Again, since  *)
(* the jugs are not calibrated, when pouring from jug A to jug B, it      *)
(* makes sense only to either fill B or empty A. And there's no point in   *)
(* emptying A if this will cause B to overflow, since that could be        *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this        *)
(* mathematically, we first define Min(m,n) to equal the minimum of the    *)
(* numbers m and n.                                                        *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n

(***************************************************************************)
(* Now we define the last two pouring actions.  From the observation       *)
(* above, these definitions should be clear.                               *)
(***************************************************************************)
SmallToBig == /\ big'   = Min(big + small, 5)
              /\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3) 
              /\ big'   = big - (small' - small)

(***************************************************************************)
(* We define the next-state relation, which I like to call Next.  A Next   *)
(* step is a step of one of the six actions defined above.  Hence, Next is *)
(* the disjunction of those actions.                                       *)
(***************************************************************************)
Next ==  \/ FillSmallJug 
         \/ FillBigJug    
         \/ EmptySmallJug 
         \/ EmptyBigJug    
         \/ SmallToBig    
         \/ BigToSmall    

(***************************************************************************)
(* We define the formula Spec to be the complete specification, asserting  *)
(* of a behavior that it begins in a state satisfying Init, and that every *)
(* step either satisfies Next or else leaves the pair <<big, small>>       *)
(* unchanged.                                                              *)
(***************************************************************************)
Spec == Init /\ [][Next]_<<big, small>> 
-----------------------------------------------------------------------------

(***************************************************************************)
(* Remember that our heroes must measure out 4 gallons of water.            *)
(* Obviously, those 4 gallons must be in the 5 gallon jug.  So, they have  *)
(* solved their problem when they reach a state with big = 4.  So, we      *)
(* define NotSolved to be the predicate asserting that big # 4.            *)
(***************************************************************************)
NotSolved == big # 4

(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant,    *)
(* which will cause it to print out an "error trace" consisting of a       *)
(* behavior ending in a states where NotSolved is false.  Such a           *)
(* behavior is the desired solution.  (Because TLC uses a breadth-first    *)
(* search, it will find the shortest solution.)                            *)
(***************************************************************************)
=============================================================================

%%file /tmp/diehard.c
#include <assert.h>


typedef enum {
    FILL_SMALL,
    FILL_BIG,
    EMPTY_SMALL,
    EMPTY_BIG,
    SMALL_TO_BIG,
    BIG_TO_SMALL,
} Action;

int min(int a, int b){
    return a < b ? a : b;
}


extern Action rand_action();



int main(){
    int big = 0;
    int small = 0;
    for(;;){
        assert(big >= 0 && big <= 5);
        assert(small >= 0 && small <= 3);
        assert(big != 4); // solved state     
        switch (rand_action()){
            case FILL_SMALL:
                small = 3;
                break;
            case FILL_BIG:
                big = 5;
                break;
            case EMPTY_SMALL:
                small = 0;
                break;
            case EMPTY_BIG:
                big = 0;
                break;
            case SMALL_TO_BIG:
                int old_big = big;
                big = min(big + small, 5);
                small -= big - old_big;
                break;
            case BIG_TO_SMALL:
                int old_small = small;
                small = min(big + small, 3);
                big -= small - old_small;
                break;
        }
    }
}

Overwriting /tmp/diehard.c

Get CBMC https://github.com/diffblue/cbmc/releases/tag/cbmc-6.3.1 . There are prepackaged versions (and a docker version).

! wget https://github.com/diffblue/cbmc/releases/download/cbmc-6.3.1/ubuntu-20.04-cbmc-6.3.1-Linux.deb && dpkg -i ubuntu-20.04-cbmc-6.3.1-Linux.deb

The color output prints kind of junky when converted to markdown for my blog :( . It looks better when you use it yourself.

! cbmc /tmp/diehard.c --unwind 7 --no-unwinding-assertions --trace

**** WARNING: Use --unwinding-assertions to obtain sound verification results
CBMC version 6.0.1 (cbmc-6.0.1-5-g54c20cdb91) 64-bit x86_64 linux
Type-checking diehard
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA


Running propositional reduction
SAT checker: instance is SATISFIABLE
Building error trace
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
/tmp/diehard.c function main
[2m[main.assertion.1] [0mline 23 assertion big >= 0 && big <= 5: [32mSUCCESS[0m
[2m[main.assertion.2] [0mline 24 assertion small >= 0 && small <= 3: [32mSUCCESS[0m
[2m[main.assertion.3] [0mline 25 assertion big != 4: [31mFAILURE[0m
[2m[main.overflow.1] [0mline 41 arithmetic overflow on signed + in big + small: [32mSUCCESS[0m
[2m[main.overflow.2] [0mline 42 arithmetic overflow on signed - in big - old_big: [32mSUCCESS[0m
[2m[main.overflow.3] [0mline 42 arithmetic overflow on signed - in small - (big - old_big): [32mSUCCESS[0m
[2m[main.overflow.4] [0mline 46 arithmetic overflow on signed + in big + small: [32mSUCCESS[0m
[2m[main.overflow.5] [0mline 47 arithmetic overflow on signed - in small - old_small: [32mSUCCESS[0m
[2m[main.overflow.6] [0mline 47 arithmetic overflow on signed - in big - (small - old_small): [32mSUCCESS[0m

Trace for main.assertion.3:

State 12 file /tmp/diehard.c function main line 20 thread 0
----------------------------------------------------
  big=0 [2m(00000000 00000000 00000000 00000000)[0m

State 14 file /tmp/diehard.c function main line 21 thread 0
----------------------------------------------------
  small=0 [2m(00000000 00000000 00000000 00000000)[0m

State 20 file /tmp/diehard.c function main line 26 thread 0
----------------------------------------------------
  return_value_rand_action=/*enum*/FILL_BIG [2m(00000000 00000000 00000000 00000001)[0m

State 23 file /tmp/diehard.c function main line 31 thread 0
----------------------------------------------------
  big=5 [2m(00000000 00000000 00000000 00000101)[0m

State 34 file /tmp/diehard.c function main line 26 thread 0
----------------------------------------------------
  return_value_rand_action=/*enum*/BIG_TO_SMALL [2m(00000000 00000000 00000000 00000101)[0m

State 42 file /tmp/diehard.c function main line 45 thread 0
----------------------------------------------------
  old_small=0 [2m(00000000 00000000 00000000 00000000)[0m

State 46 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  a=5 [2m(00000000 00000000 00000000 00000101)[0m

State 47 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  b=3 [2m(00000000 00000000 00000000 00000011)[0m

State 48 file /tmp/diehard.c function min line 14 thread 0
----------------------------------------------------
  goto_symex$$return_value$$min=3 [2m(00000000 00000000 00000000 00000011)[0m

State 50 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  small=3 [2m(00000000 00000000 00000000 00000011)[0m

State 53 file /tmp/diehard.c function main line 47 thread 0
----------------------------------------------------
  big=2 [2m(00000000 00000000 00000000 00000010)[0m

State 63 file /tmp/diehard.c function main line 26 thread 0
----------------------------------------------------
  return_value_rand_action=/*enum*/EMPTY_SMALL [2m(00000000 00000000 00000000 00000010)[0m

State 67 file /tmp/diehard.c function main line 34 thread 0
----------------------------------------------------
  small=0 [2m(00000000 00000000 00000000 00000000)[0m

State 78 file /tmp/diehard.c function main line 26 thread 0
----------------------------------------------------
  return_value_rand_action=/*enum*/BIG_TO_SMALL [2m(00000000 00000000 00000000 00000101)[0m

State 86 file /tmp/diehard.c function main line 45 thread 0
----------------------------------------------------
  old_small=0 [2m(00000000 00000000 00000000 00000000)[0m

State 90 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  a=2 [2m(00000000 00000000 00000000 00000010)[0m

State 91 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  b=3 [2m(00000000 00000000 00000000 00000011)[0m

State 92 file /tmp/diehard.c function min line 14 thread 0
----------------------------------------------------
  goto_symex$$return_value$$min=2 [2m(00000000 00000000 00000000 00000010)[0m

State 94 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  small=2 [2m(00000000 00000000 00000000 00000010)[0m

State 97 file /tmp/diehard.c function main line 47 thread 0
----------------------------------------------------
  big=0 [2m(00000000 00000000 00000000 00000000)[0m

State 107 file /tmp/diehard.c function main line 26 thread 0
----------------------------------------------------
  return_value_rand_action=/*enum*/FILL_BIG [2m(00000000 00000000 00000000 00000001)[0m

State 110 file /tmp/diehard.c function main line 31 thread 0
----------------------------------------------------
  big=5 [2m(00000000 00000000 00000000 00000101)[0m

State 121 file /tmp/diehard.c function main line 26 thread 0
----------------------------------------------------
  return_value_rand_action=/*enum*/BIG_TO_SMALL [2m(00000000 00000000 00000000 00000101)[0m

State 129 file /tmp/diehard.c function main line 45 thread 0
----------------------------------------------------
  old_small=2 [2m(00000000 00000000 00000000 00000010)[0m

State 133 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  a=7 [2m(00000000 00000000 00000000 00000111)[0m

State 134 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  b=3 [2m(00000000 00000000 00000000 00000011)[0m

State 135 file /tmp/diehard.c function min line 14 thread 0
----------------------------------------------------
  goto_symex$$return_value$$min=3 [2m(00000000 00000000 00000000 00000011)[0m

State 137 file /tmp/diehard.c function main line 46 thread 0
----------------------------------------------------
  small=3 [2m(00000000 00000000 00000000 00000011)[0m

State 140 file /tmp/diehard.c function main line 47 thread 0
----------------------------------------------------
  big=4 [2m(00000000 00000000 00000000 00000100)[0m

[31mViolated property:[0m
  file /tmp/diehard.c function main line 25 thread 0
  [31massertion big != 4[0m
  big != 4



** 1 of 9 failed (2 iterations)
VERIFICATION FAILED

Concurrent Bank Account Example

Ok, but many of the things I might want to use TLA+ for are concurrent processes.

If you write your C simulator in the right style, this is not hard to model.

TLA+ offers an imperative syntax called PlusCal that compiles down to the logical specification. You have to write your C simulator in a related style.

Each process has a state which crucially includes a “program counter”. It is easy to forget sometimes that a program counter is a thing because C and other high level languages make it implicit. But it is there and it is useful.

https://learntla.com/intro/conceptual-overview.html

%%file /tmp/wire.tla

---- MODULE wire ----
EXTENDS TLC, Integers

People == {"alice", "bob"}
Money == 1..10
NumTransfers == 2

(* --algorithm wire
variables
  acct \in [People -> Money];

define
  NoOverdrafts ==
    \A p \in People:
      acct[p] >= 0
end define;

process wire \in 1..NumTransfers
variable
  amnt \in 1..5;
  from \in People;
  to \in People
begin
  Check:
    if acct[from] >= amnt then
      Withdraw:
        acct[from] := acct[from] - amnt;
      Deposit:
        acct[to] := acct[to] + amnt;
    end if;
end process;
end algorithm; *)

====

Writing /tmp/wire.tla

Here I’m going to run TLA+ in command line mode as described here https://learntla.com/topics/cli.html

%%file /tmp/wire.cfg
SPECIFICATION Spec

INVARIANT NoOverdrafts

! cd /tmp && wget https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar #install tla+

--2024-10-07 20:35:54--  https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
Resolving github.com (github.com)... 140.82.113.4
Connecting to github.com (github.com)|140.82.113.4|:443... connected.
HTTP request sent, awaiting response... 302 Found
Location: https://objects.githubusercontent.com/github-production-release-asset-2e65be/50906927/b215e7c4-2d49-49c9-bcfa-634e26027bdf?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=releaseassetproduction%2F20241008%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Date=20241008T003554Z&X-Amz-Expires=300&X-Amz-Signature=ba93c3533e3330f9a278185ab99fab8abbeb21d4c33be0a409e73cabc6999a43&X-Amz-SignedHeaders=host&response-content-disposition=attachment%3B%20filename%3Dtla2tools.jar&response-content-type=application%2Foctet-stream [following]
--2024-10-07 20:35:54--  https://objects.githubusercontent.com/github-production-release-asset-2e65be/50906927/b215e7c4-2d49-49c9-bcfa-634e26027bdf?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=releaseassetproduction%2F20241008%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Date=20241008T003554Z&X-Amz-Expires=300&X-Amz-Signature=ba93c3533e3330f9a278185ab99fab8abbeb21d4c33be0a409e73cabc6999a43&X-Amz-SignedHeaders=host&response-content-disposition=attachment%3B%20filename%3Dtla2tools.jar&response-content-type=application%2Foctet-stream
Resolving objects.githubusercontent.com (objects.githubusercontent.com)... 185.199.109.133, 185.199.108.133, 185.199.110.133, ...
Connecting to objects.githubusercontent.com (objects.githubusercontent.com)|185.199.109.133|:443... connected.
HTTP request sent, awaiting response... 200 OK
Length: 2274532 (2.2M) [application/octet-stream]
Saving to: ‘tla2tools.jar’

tla2tools.jar       100%[===================>]   2.17M  --.-KB/s    in 0.09s   

2024-10-07 20:35:54 (24.1 MB/s) - ‘tla2tools.jar’ saved [2274532/2274532]

%%bash
cd /tmp
java -cp tla2tools.jar pcal.trans wire.tla
java -jar tla2tools.jar -config wire.cfg wire.tla

pcal.trans Version 1.11 of 31 December 2020
Parsing completed.
Translation completed.
New file wire.tla written.
New file wire.cfg written.


TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
Warning: Please run the Java VM which executes TLC with a throughput optimized garbage collector by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 68 and seed -4391951418103122557 with 1 worker on 16 cores with 15752MB heap and 64MB offheap memory [pid: 594435] (Linux 6.5.0-1027-oem amd64, Ubuntu 21.0.4 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/wire.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module wire
Starting... (2024-10-07 20:41:25)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Computed 1024 initial states...
Computed 2048 initial states...
Computed 4096 initial states...
Computed 8192 initial states...
Computed 16384 initial states...
Computed 32768 initial states...
Finished computing initial states: 40000 distinct states generated at 2024-10-07 20:41:25.
Error: Invariant NoOverdrafts is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ acct = [alice |-> 1, bob |-> 1]
/\ amnt = <<1, 1>>
/\ to = <<"alice", "alice">>
/\ from = <<"alice", "alice">>
/\ pc = <<"Check", "Check">>

State 2: <Check line 56, col 16 to line 60, col 54 of module wire>
/\ acct = [alice |-> 1, bob |-> 1]
/\ amnt = <<1, 1>>
/\ to = <<"alice", "alice">>
/\ from = <<"alice", "alice">>
/\ pc = <<"Withdraw", "Check">>

State 3: <Check line 56, col 16 to line 60, col 54 of module wire>
/\ acct = [alice |-> 1, bob |-> 1]
/\ amnt = <<1, 1>>
/\ to = <<"alice", "alice">>
/\ from = <<"alice", "alice">>
/\ pc = <<"Withdraw", "Withdraw">>

State 4: <Withdraw line 62, col 19 to line 65, col 51 of module wire>
/\ acct = [alice |-> 0, bob |-> 1]
/\ amnt = <<1, 1>>
/\ to = <<"alice", "alice">>
/\ from = <<"alice", "alice">>
/\ pc = <<"Deposit", "Withdraw">>

State 5: <Withdraw line 62, col 19 to line 65, col 51 of module wire>
/\ acct = [alice |-> -1, bob |-> 1]
/\ amnt = <<1, 1>>
/\ to = <<"alice", "alice">>
/\ from = <<"alice", "alice">>
/\ pc = <<"Deposit", "Deposit">>

459204 states generated, 356003 distinct states found, 131999 states left on queue.
The depth of the complete state graph search is 5.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
Finished in 01s at (2024-10-07 20:41:26)



---------------------------------------------------------------------------

CalledProcessError                        Traceback (most recent call last)

Cell In[85], line 1
----> 1 get_ipython().run_cell_magic('bash', '', 'cd /tmp\njava -cp tla2tools.jar pcal.trans wire.tla\njava -jar tla2tools.jar -config wire.cfg wire.tla\n')


File ~/.local/lib/python3.10/site-packages/IPython/core/interactiveshell.py:2541, in InteractiveShell.run_cell_magic(self, magic_name, line, cell)
   2539 with self.builtin_trap:
   2540     args = (magic_arg_s, cell)
-> 2541     result = fn(*args, **kwargs)
   2543 # The code below prevents the output from being displayed
   2544 # when using magics with decorator @output_can_be_silenced
   2545 # when the last Python token in the expression is a ';'.
   2546 if getattr(fn, magic.MAGIC_OUTPUT_CAN_BE_SILENCED, False):


File ~/.local/lib/python3.10/site-packages/IPython/core/magics/script.py:155, in ScriptMagics._make_script_magic.<locals>.named_script_magic(line, cell)
    153 else:
    154     line = script
--> 155 return self.shebang(line, cell)


File ~/.local/lib/python3.10/site-packages/IPython/core/magics/script.py:315, in ScriptMagics.shebang(self, line, cell)
    310 if args.raise_error and p.returncode != 0:
    311     # If we get here and p.returncode is still None, we must have
    312     # killed it but not yet seen its return code. We don't wait for it,
    313     # in case it's stuck in uninterruptible sleep. -9 = SIGKILL
    314     rc = p.returncode or -9
--> 315     raise CalledProcessError(rc, cell)


CalledProcessError: Command 'b'cd /tmp\njava -cp tla2tools.jar pcal.trans wire.tla\njava -jar tla2tools.jar -config wire.cfg wire.tla\n'' returned non-zero exit status 12.

The example here is just having two calls to withdrawing from Alice. Pretty simple.

Here is an attempt at a similar C program.

It has to be written in a somewhat odd style.

Finagling C ints is actually super painful. It is also a bit verbose

%%file /tmp/bank.c

#include <assert.h>
#include <stdint.h>
#include <stdbool.h>

#define NumTransfers 2


#define PeopleCount 2
typedef enum { ALICE = 0, BOB = 1 } People;

typedef int8_t Money;

typedef enum { Check, Withdraw, Deposit, Done } Action;

typedef struct {
    People from;
    People to;
    Money amnt;
    Action label;
} procstate_t;

// Global state variables
// Basically arrays seem like ok stand ins for TLA+ key value maps
Money acct[PeopleCount];

procstate_t proc_states[NumTransfers];

extern uint8_t rand_proc();
extern Money rand_money() __CPROVER_ensures(__CPROVER_return_value >= 0 && __CPROVER_return_value <= 5);

// Function to initialize the process states
void initialize_processes() {
    for(int p = 0; p < PeopleCount; p++) {
        Money m = rand_money();
        m = m < 0 ? 0 : m % 10;
        acct[p] = m;
    }
    for (int i = 0; i < NumTransfers; i++) {
        //proc_states[i].from %= PeopleCount;
        //proc_states[i].to %= PeopleCount;
        proc_states[i].label = Check;
        proc_states[i].amnt = rand_money() % 5 + 4;   
    }
}


void wire(uint8_t procnum) 
__CPROVER_requires(procnum < NumTransfers)
{
    procstate_t *p = &(proc_states[procnum]);
    //printf("procnum: %d, from: %d, to: %d, amnt: %d, label: %d\n", procnum, p->from, p->to, p->amnt, p->label);
    switch (p->label) {
        case Check:
            if (acct[p->from] >= p->amnt) {
                p->label = Withdraw;
            } else {
                p->label = Done;
            }
            break;
        case Withdraw:
            acct[p->from] -= p->amnt;
            p->label = Deposit;
            break;
        case Deposit:
            acct[p->to] += p->amnt;
            p->label = Done;
            break;
        case Done:
            break;
    }
}

void check_no_overdrafts() {
    for (int p = 0; p < PeopleCount; p++) {
        // No account should have a negative balance
        assert(acct[p] >= 0);
    }
}

int main() {
    initialize_processes();
    for(;;){
        wire(rand_proc() % NumTransfers);
        check_no_overdrafts();
    }
}

Overwriting /tmp/bank.c

!cbmc /tmp/bank.c --unwind 10

CBMC version 6.0.1 (cbmc-6.0.1-5-g54c20cdb91) 64-bit x86_64 linux
Type-checking bank
file /tmp/bank.c line 52 function wire: function 'printf' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-printf> line 14: implicit function declaration 'printf'
old definition in module bank file /tmp/bank.c line 52 function wire
signed int (void)
new definition in module <built-in-library> file <builtin-library-printf> line 14
signed int (const char *format, ...)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking


Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker inconsistent: instance is UNSATISFIABLE

** Results:
/tmp/bank.c function check_no_overdrafts
[2m[check_no_overdrafts.overflow.1] [0mline 75 arithmetic overflow on signed + in p + 1: [32mSUCCESS[0m
[2m[check_no_overdrafts.array_bounds.1] [0mline 77 array 'acct' lower bound in acct[(signed long int)p]: [32mSUCCESS[0m
[2m[check_no_overdrafts.array_bounds.2] [0mline 77 array 'acct' upper bound in acct[(signed long int)p]: [32mSUCCESS[0m
[2m[check_no_overdrafts.assertion.1] [0mline 77 assertion acct[p] >= 0: [31mFAILURE[0m

/tmp/bank.c function initialize_processes
[2m[initialize_processes.overflow.1] [0mline 34 arithmetic overflow on signed + in p + 1: [32mSUCCESS[0m
[2m[initialize_processes.no-body.rand_money] [0mline 35 no body for callee rand_money: [31mFAILURE[0m
[2m[initialize_processes.array_bounds.1] [0mline 37 array 'acct' lower bound in acct[(signed long int)p]: [32mSUCCESS[0m
[2m[initialize_processes.array_bounds.2] [0mline 37 array 'acct' upper bound in acct[(signed long int)p]: [32mSUCCESS[0m
[2m[initialize_processes.overflow.3] [0mline 39 arithmetic overflow on signed + in i + 1: [32mSUCCESS[0m
[2m[initialize_processes.array_bounds.3] [0mline 42 array 'proc_states' lower bound in proc_states[(signed long int)i]: [32mSUCCESS[0m
[2m[initialize_processes.array_bounds.4] [0mline 42 array 'proc_states' upper bound in proc_states[(signed long int)i]: [32mSUCCESS[0m
[2m[initialize_processes.array_bounds.5] [0mline 43 array 'proc_states' lower bound in proc_states[(signed long int)i]: [32mSUCCESS[0m
[2m[initialize_processes.array_bounds.6] [0mline 43 array 'proc_states' upper bound in proc_states[(signed long int)i]: [32mSUCCESS[0m
[2m[initialize_processes.overflow.2] [0mline 43 arithmetic overflow on signed + in (signed int)return_value_rand_money$0 % 5 + 4: [32mSUCCESS[0m

/tmp/bank.c function main
[2m[main.unwind.0] [0mline 83 unwinding assertion loop 0: [31mFAILURE[0m
[2m[main.no-body.rand_proc] [0mline 84 no body for callee rand_proc: [31mFAILURE[0m

/tmp/bank.c function wire
[2m[wire.pointer_dereference.1] [0mline 52 dereference failure: pointer outside object bounds in p->from: [32mSUCCESS[0m
[2m[wire.pointer_dereference.2] [0mline 52 dereference failure: pointer outside object bounds in p->to: [32mSUCCESS[0m
[2m[wire.pointer_dereference.3] [0mline 52 dereference failure: pointer outside object bounds in p->amnt: [32mSUCCESS[0m
[2m[wire.pointer_dereference.4] [0mline 52 dereference failure: pointer outside object bounds in p->label: [32mSUCCESS[0m
[2m[wire.pointer_dereference.5] [0mline 53 dereference failure: pointer outside object bounds in p->label: [32mSUCCESS[0m
[2m[wire.array_bounds.1] [0mline 55 array 'acct' lower bound in acct[(signed long int)p->from]: [32mSUCCESS[0m
[2m[wire.array_bounds.2] [0mline 55 array 'acct' upper bound in acct[(signed long int)p->from]: [32mSUCCESS[0m
[2m[wire.pointer_dereference.6] [0mline 55 dereference failure: pointer outside object bounds in p->from: [32mSUCCESS[0m
[2m[wire.pointer_dereference.7] [0mline 55 dereference failure: pointer outside object bounds in p->amnt: [32mSUCCESS[0m
[2m[wire.pointer_dereference.8] [0mline 56 dereference failure: pointer outside object bounds in p->label: [32mSUCCESS[0m
[2m[wire.pointer_dereference.9] [0mline 58 dereference failure: pointer outside object bounds in p->label: [32mSUCCESS[0m
[2m[wire.array_bounds.3] [0mline 62 array 'acct' lower bound in acct[(signed long int)p->from]: [32mSUCCESS[0m
[2m[wire.array_bounds.4] [0mline 62 array 'acct' upper bound in acct[(signed long int)p->from]: [32mSUCCESS[0m
[2m[wire.overflow.1] [0mline 62 arithmetic overflow on signed - in (signed int)acct[(signed long int)p->from] - (signed int)p->amnt: [32mSUCCESS[0m
[2m[wire.pointer_dereference.10] [0mline 62 dereference failure: pointer outside object bounds in p->from: [32mSUCCESS[0m
[2m[wire.pointer_dereference.11] [0mline 62 dereference failure: pointer outside object bounds in p->amnt: [32mSUCCESS[0m
[2m[wire.pointer_dereference.12] [0mline 63 dereference failure: pointer outside object bounds in p->label: [32mSUCCESS[0m
[2m[wire.array_bounds.5] [0mline 66 array 'acct' lower bound in acct[(signed long int)p->to]: [32mSUCCESS[0m
[2m[wire.array_bounds.6] [0mline 66 array 'acct' upper bound in acct[(signed long int)p->to]: [32mSUCCESS[0m
[2m[wire.overflow.2] [0mline 66 arithmetic overflow on signed + in (signed int)acct[(signed long int)p->to] + (signed int)p->amnt: [32mSUCCESS[0m
[2m[wire.pointer_dereference.13] [0mline 66 dereference failure: pointer outside object bounds in p->to: [32mSUCCESS[0m
[2m[wire.pointer_dereference.14] [0mline 66 dereference failure: pointer outside object bounds in p->amnt: [32mSUCCESS[0m
[2m[wire.pointer_dereference.15] [0mline 67 dereference failure: pointer outside object bounds in p->label: [32mSUCCESS[0m

** 4 of 39 failed (3 iterations)
VERIFICATION FAILED

We can narrow down on the only property we care about. This trace is much harder to read than the above.

!cbmc /tmp/bank.c  --unwind 10 --property  check_no_overdrafts.assertion.1 --no-unwinding-assertions --no-standard-checks --compact-trace

**** WARNING: Use --unwinding-assertions to obtain sound verification results
CBMC version 6.0.1 (cbmc-6.0.1-5-g54c20cdb91) 64-bit x86_64 linux
Type-checking bank
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking


Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Building error trace

** Results:
/tmp/bank.c function check_no_overdrafts
[2m[check_no_overdrafts.assertion.1] [0mline 77 assertion acct[p] >= 0: [31mFAILURE[0m

Trace for check_no_overdrafts.assertion.1:
  [2m25:[0m acct[0l]=0 [2m(00000000)[0m
  [2m25:[0m acct[1l]=0 [2m(00000000)[0m
  [2m27:[0m proc_states[0l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=0,
    .$pad3=0, .label=/*enum*/Check } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000, 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 })[0m
  [2m27:[0m proc_states[0l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[0l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[0l].amnt=0 [2m(00000000)[0m
  [2m27:[0m proc_states[0l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[0l].label=/*enum*/Check [2m(00000000 00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[1l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=0,
    .$pad3=0, .label=/*enum*/Check } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000, 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 })[0m
  [2m27:[0m proc_states[1l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[1l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[1l].amnt=0 [2m(00000000)[0m
  [2m27:[0m proc_states[1l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m27:[0m proc_states[1l].label=/*enum*/Check [2m(00000000 00000000 00000000 00000000)[0m

[2m↳[0m [2m/tmp/bank.c[2m:81[0m main()

[2m↳[0m [2m/tmp/bank.c[2m:82[0m initialize_processes()
  [2m34:[0m p=0 [2m(00000000 00000000 00000000 00000000)[0m

[2m↳[0m [2m/tmp/bank.c[2m:35[0m rand_money()
[2m↵[0m
  [2m35:[0m return_value_rand_money='\t' [2m(00001001)[0m
  [2m35:[0m m='\t' [2m(00001001)[0m
  [2m36:[0m m='\t' [2m(00001001)[0m
  [2m37:[0m acct[0l]='\t' [2m(00001001)[0m
  [2m34:[0m p=1 [2m(00000000 00000000 00000000 00000001)[0m

[2m↳[0m [2m/tmp/bank.c[2m:35[0m rand_money()
[2m↵[0m
  [2m35:[0m return_value_rand_money=1 [2m(00000001)[0m
  [2m35:[0m m=1 [2m(00000001)[0m
  [2m36:[0m m=1 [2m(00000001)[0m
  [2m37:[0m acct[1l]=1 [2m(00000001)[0m
  [2m34:[0m p=2 [2m(00000000 00000000 00000000 00000010)[0m
  [2m39:[0m i=0 [2m(00000000 00000000 00000000 00000000)[0m
  [2m42:[0m proc_states[0l].label=/*enum*/Check [2m(00000000 00000000 00000000 00000000)[0m

[2m↳[0m [2m/tmp/bank.c[2m:43[0m rand_money()
[2m↵[0m
  [2m43:[0m return_value_rand_money$0=')' [2m(00101001)[0m
  [2m43:[0m proc_states[0l].amnt=5 [2m(00000101)[0m
  [2m39:[0m i=1 [2m(00000000 00000000 00000000 00000001)[0m
  [2m42:[0m proc_states[1l].label=/*enum*/Check [2m(00000000 00000000 00000000 00000000)[0m

[2m↳[0m [2m/tmp/bank.c[2m:43[0m rand_money()
[2m↵[0m
  [2m43:[0m return_value_rand_money$0=18 [2m(00010010)[0m
  [2m43:[0m proc_states[1l].amnt=7 [2m(00000111)[0m
  [2m39:[0m i=2 [2m(00000000 00000000 00000000 00000010)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m rand_proc()
[2m↵[0m
  [2m84:[0m return_value_rand_proc=1 [2m(00000001)[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m wire(1)
  [2m51:[0m p=proc_states + 1l [2m(00000010 00000000 00000000 00000000 00000000 00000000 00000000 00010000)[0m
  [2m56:[0m byte_extract_little_endian(proc_states, 12l + (signed long int)__CPROVER_POINTER_OFFSET(p), Action)=byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Check }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, 12l + (signed long int)__CPROVER_POINTER_OFFSET(proc_states + 1l), Action) [2m(?)[0m
  [2m56:[0m proc_states[0l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Check } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000101, 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 })[0m
  [2m56:[0m proc_states[0l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[0l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[0l].amnt=5 [2m(00000101)[0m
  [2m56:[0m proc_states[0l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[0l].label=/*enum*/Check [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000111, 00000000 00000000 00000000, 00000000 00000000 00000000 00000001 })[0m
  [2m56:[0m proc_states[1l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l].amnt=7 [2m(00000111)[0m
  [2m56:[0m proc_states[1l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l].label=/*enum*/Withdraw [2m(00000000 00000000 00000000 00000001)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:85[0m check_no_overdrafts()
  [2m75:[0m p=0 [2m(00000000 00000000 00000000 00000000)[0m
  [2m75:[0m p=1 [2m(00000000 00000000 00000000 00000001)[0m
  [2m75:[0m p=2 [2m(00000000 00000000 00000000 00000010)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m rand_proc()
[2m↵[0m
  [2m84:[0m return_value_rand_proc=32 [2m(00100000)[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m wire(0)
  [2m51:[0m p=proc_states [2m(00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)[0m
  [2m56:[0m byte_extract_little_endian(proc_states, 12l + (signed long int)__CPROVER_POINTER_OFFSET(p), Action)=byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Withdraw }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, 12l + (signed long int)__CPROVER_POINTER_OFFSET(proc_states), Action) [2m(?)[0m
  [2m56:[0m proc_states[0l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Withdraw } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000101, 00000000 00000000 00000000, 00000000 00000000 00000000 00000001 })[0m
  [2m56:[0m proc_states[0l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[0l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[0l].amnt=5 [2m(00000101)[0m
  [2m56:[0m proc_states[0l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[0l].label=/*enum*/Withdraw [2m(00000000 00000000 00000000 00000001)[0m
  [2m56:[0m proc_states[1l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000111, 00000000 00000000 00000000, 00000000 00000000 00000000 00000001 })[0m
  [2m56:[0m proc_states[1l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l].amnt=7 [2m(00000111)[0m
  [2m56:[0m proc_states[1l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m56:[0m proc_states[1l].label=/*enum*/Withdraw [2m(00000000 00000000 00000000 00000001)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:85[0m check_no_overdrafts()
  [2m75:[0m p=0 [2m(00000000 00000000 00000000 00000000)[0m
  [2m75:[0m p=1 [2m(00000000 00000000 00000000 00000001)[0m
  [2m75:[0m p=2 [2m(00000000 00000000 00000000 00000010)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m rand_proc()
[2m↵[0m
  [2m84:[0m return_value_rand_proc=154 [2m(10011010)[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m wire(0)
  [2m51:[0m p=proc_states [2m(00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)[0m
  [2m62:[0m acct[(signed long int)byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Withdraw }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, (signed long int)__CPROVER_POINTER_OFFSET(proc_states), People)]={ 4, 1 }[(signed long int)byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Withdraw }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, (signed long int)__CPROVER_POINTER_OFFSET(proc_states), People)] [2m(?)[0m
  [2m62:[0m acct[0l]=4 [2m(00000100)[0m
  [2m62:[0m acct[1l]=1 [2m(00000001)[0m
  [2m63:[0m byte_extract_little_endian(proc_states, 12l + (signed long int)__CPROVER_POINTER_OFFSET(p), Action)=byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Deposit }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, 12l + (signed long int)__CPROVER_POINTER_OFFSET(proc_states), Action) [2m(?)[0m
  [2m63:[0m proc_states[0l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Deposit } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000101, 00000000 00000000 00000000, 00000000 00000000 00000000 00000010 })[0m
  [2m63:[0m proc_states[0l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[0l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[0l].amnt=5 [2m(00000101)[0m
  [2m63:[0m proc_states[0l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[0l].label=/*enum*/Deposit [2m(00000000 00000000 00000000 00000010)[0m
  [2m63:[0m proc_states[1l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000111, 00000000 00000000 00000000, 00000000 00000000 00000000 00000001 })[0m
  [2m63:[0m proc_states[1l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[1l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[1l].amnt=7 [2m(00000111)[0m
  [2m63:[0m proc_states[1l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[1l].label=/*enum*/Withdraw [2m(00000000 00000000 00000000 00000001)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:85[0m check_no_overdrafts()
  [2m75:[0m p=0 [2m(00000000 00000000 00000000 00000000)[0m
  [2m75:[0m p=1 [2m(00000000 00000000 00000000 00000001)[0m
  [2m75:[0m p=2 [2m(00000000 00000000 00000000 00000010)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m rand_proc()
[2m↵[0m
  [2m84:[0m return_value_rand_proc=1 [2m(00000001)[0m

[2m↳[0m [2m/tmp/bank.c[2m:84[0m wire(1)
  [2m51:[0m p=proc_states + 1l [2m(00000010 00000000 00000000 00000000 00000000 00000000 00000000 00010000)[0m
  [2m62:[0m acct[(signed long int)byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Deposit }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, (signed long int)__CPROVER_POINTER_OFFSET(proc_states + 1l), People)]={ -3, 1 }[(signed long int)byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Deposit }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Withdraw } }, (signed long int)__CPROVER_POINTER_OFFSET(proc_states + 1l), People)] [2m(?)[0m
  [2m62:[0m acct[0l]=-3 [2m(11111101)[0m
  [2m62:[0m acct[1l]=1 [2m(00000001)[0m
  [2m63:[0m byte_extract_little_endian(proc_states, 12l + (signed long int)__CPROVER_POINTER_OFFSET(p), Action)=byte_extract_little_endian({ { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Deposit }, 
    { .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Deposit } }, 12l + (signed long int)__CPROVER_POINTER_OFFSET(proc_states + 1l), Action) [2m(?)[0m
  [2m63:[0m proc_states[0l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=5,
    .$pad3=0, .label=/*enum*/Deposit } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000101, 00000000 00000000 00000000, 00000000 00000000 00000000 00000010 })[0m
  [2m63:[0m proc_states[0l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[0l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[0l].amnt=5 [2m(00000101)[0m
  [2m63:[0m proc_states[0l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[0l].label=/*enum*/Deposit [2m(00000000 00000000 00000000 00000010)[0m
  [2m63:[0m proc_states[1l]={ .from=/*enum*/ALICE, .to=/*enum*/ALICE, .amnt=7,
    .$pad3=0, .label=/*enum*/Deposit } [2m({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000111, 00000000 00000000 00000000, 00000000 00000000 00000000 00000010 })[0m
  [2m63:[0m proc_states[1l].from=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[1l].to=/*enum*/ALICE [2m(00000000 00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[1l].amnt=7 [2m(00000111)[0m
  [2m63:[0m proc_states[1l].$pad3=0 [2m(00000000 00000000 00000000)[0m
  [2m63:[0m proc_states[1l].label=/*enum*/Deposit [2m(00000000 00000000 00000000 00000010)[0m
[2m↵[0m

[2m↳[0m [2m/tmp/bank.c[2m:85[0m check_no_overdrafts()
  [2m75:[0m p=0 [2m(00000000 00000000 00000000 00000000)[0m

[31mViolated property:[0m
  file /tmp/bank.c function check_no_overdrafts line 77 thread 0
  [31massertion acct[p] >= 0[0m
  (signed int)acct[(signed long int)p] >= 0



** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

Bits and Bobbles

Ok. Interesting experiment. It was not nearly as easy to do the second puzzle as I’d hoped.

The C version does add enough kludge and disclarity that is entirely avoidable.

I think one could get in the groove and clean up the C code to be more like the TLA+ code.

Using static inside of C functions is way to do coroutine like things https://stackoverflow.com/questions/572547/what-does-static-mean-in-c It might make for nice looking code. It’s more or less the same as global variables.

If we package up all the state into a single struct, we could imagine hashing it and doing a breadth first search.

SPIN is pretty nice. It is C ish and can embed C.

deadlock empire examples https://deadlockempire.github.io/ https://github.com/cobusve/TLAPLUS_DeadlockEmpire

TLA+ futex https://surfingcomplexity.blog/2024/10/05/futexes-in-tla/

I once did a project using https://omnetpp.org/ as a network simulator. CBMC will never one-shot scale to that.

These are very simple starter TLA+ examples. I am not a TLA+ power user. I’ve heard tale that there are some very nice features that feel essential.

I did not do a liveness property. I’m not sure how I would really. I think about safety more often.

One can use __CPROVER_assume annotations to do the TLA+ style transition relation instead of an imperative style also.

Maybe Kani (the rust equivlent of CBMC) would be easier?

There is a spectrum of different levels of assurance in software verification.

The hard core stuff is using interactive theorem provers like Lean, Coq, Isabelle. It is maximally expressive with lots of proof burden.

You can also try to really connect your model up to your implementation as different levels of fineness.

High level models are often easier to check and prove things about. For concurrent or distributed systems, even these high level models can easily hold bugs, and there is benefit to exercising them.

Sometimes you can think of this as being at the protocol level. The sort of thing that might be a diagram in some document rather than the source code itself.

CBMC is the C based model checker. It is designed to symbolically execute C source code and check for bugs. It aims to be sound (with assumptions and caveats). If CBMC finishes all green, there really shouldn’t be certain classes of bugs in the program.

Fuzzing tools are very effective, but it is a weaker guarantee if they come back all green.