Formal Verification Guide

--------------------------- MODULE TwoPhaseCommit -------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS RM  \* Set of resource managers

VARIABLES
    rmState,      \* rmState[r] is the state of resource manager r
    tmState,      \* State of the transaction manager
    tmPrepared,   \* Set of RMs that have sent "Prepared"
    msgs          \* Set of messages sent

vars == <<rmState, tmState, tmPrepared, msgs>>

Init ==
    /\ rmState = [r \in RM |-> "working"]
    /\ tmState = "init"
    /\ tmPrepared = {}
    /\ msgs = {}

\* RM r prepares to commit
RMPrepare(r) ==
    /\ rmState[r] = "working"
    /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
    /\ msgs' = msgs \union {[type |-> "Prepared", rm |-> r]}
    /\ UNCHANGED <<tmState, tmPrepared>>

\* TM receives a Prepared message from RM r
TMRcvPrepared(r) ==
    /\ tmState = "init"
    /\ [type |-> "Prepared", rm |-> r] \in msgs
    /\ tmPrepared' = tmPrepared \union {r}
    /\ UNCHANGED <<rmState, tmState, msgs>>

\* TM commits (all RMs have prepared)
TMCommit ==
    /\ tmState = "init"
    /\ tmPrepared = RM
    /\ tmState' = "committed"
    /\ msgs' = msgs \union {[type |-> "Commit"]}
    /\ UNCHANGED <<rmState, tmPrepared>>

\* Safety property: No RM commits unless TM has committed
Consistency ==
    \A r \in RM : rmState[r] = "committed" => tmState = "committed"
========================================================================

# Install TLA+ Toolbox or use command-line TLC
# Define model with specific constants
# RM = {"rm1", "rm2", "rm3"}
java -jar tla2tools.jar -config TwoPhaseCommit.cfg TwoPhaseCommit.tla

# TLC will explore all reachable states and verify:
# - No deadlocks (unless specified)
# - Safety properties (invariants)
# - Liveness properties (temporal formulas)

(* Example: Proving properties of a simple functional program *)

(* Define natural number addition *)
Fixpoint add (n m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (add n' m)
  end.

(* Prove: 0 + n = n (left identity) *)
Theorem add_0_l : forall n : nat, add 0 n = n.
Proof.
  intro n.
  simpl.    (* simplification reduces add 0 n to n *)
  reflexivity.
Qed.

(* Prove: n + 0 = n (right identity, requires induction) *)
Theorem add_0_r : forall n : nat, add n 0 = n.
Proof.
  intro n.
  induction n as [| n' IHn'].
  - (* Base case: n = 0 *)
    simpl. reflexivity.
  - (* Inductive step: n = S n' *)
    simpl.               (* add (S n') 0 = S (add n' 0) *)
    rewrite IHn'.        (* apply induction hypothesis *)
    reflexivity.
Qed.

(* Prove associativity of addition *)
Theorem add_assoc : forall a b c : nat,
  add a (add b c) = add (add a b) c.
Proof.
  intros a b c.
  induction a as [| a' IHa'].
  - simpl. reflexivity.
  - simpl. rewrite IHa'. reflexivity.
Qed.

theory SimpleVerification
  imports Main
begin

(* Define a recursive function *)
fun fib :: "nat => nat" where
  "fib 0 = 0"
| "fib (Suc 0) = 1"
| "fib (Suc (Suc n)) = fib (Suc n) + fib n"

(* Prove a property *)
lemma fib_positive: "0 < fib (Suc n)"
  by (induction n rule: fib.induct) auto

(* Verify a sorting algorithm *)
fun insert :: "nat => nat list => nat list" where
  "insert x [] = [x]"
| "insert x (y # ys) = (if x <= y then x # y # ys else y # insert x ys)"

fun isort :: "nat list => nat list" where
  "isort [] = []"
| "isort (x # xs) = insert x (isort xs)"

(* Prove the output is sorted *)
lemma sorted_insert: "sorted (insert x xs) = sorted xs"
  sorry (* full proof requires additional lemmas *)

end

from z3 import Solver, Int, Bool, And, Or, Not, Implies, ForAll, sat, unsat

def verify_array_bounds():
    """
    Verify that an array access is always within bounds.
    Model a loop: for i = 0 to n-1, access a[i].
    """
    s = Solver()
    n = Int("n")
    i = Int("i")

    # Precondition: n > 0
    s.add(n > 0)

    # Loop invariant: 0 <= i < n at each access
    s.add(i >= 0)
    s.add(i < n)

    # Verify: the access a[i] is within bounds [0, n)
    s.add(Not(And(i >= 0, i < n)))  # try to find a violation

    result = s.check()
    if result == unsat:
        return "VERIFIED: array access is always within bounds"
    else:
        return f"COUNTEREXAMPLE: {s.model()}"

def verify_integer_overflow():
    """
    Check if integer addition can overflow for given constraints.
    """
    from z3 import BitVec, BitVecVal

    s = Solver()
    # 32-bit signed integers
    x = BitVec("x", 32)
    y = BitVec("y", 32)

    # Preconditions: both positive
    s.add(x > 0)
    s.add(y > 0)

    # Check: can x + y wrap around to negative?
    s.add(x + y < 0)

    if s.check() == sat:
        m = s.model()
        return {
            "overflow_possible": True,
            "x": m[x].as_long(),
            "y": m[y].as_long(),
        }
    return {"overflow_possible": False}

/* Mutual exclusion with Peterson's algorithm */
bool flag[2] = false;
byte turn = 0;
byte critical = 0;  /* count of processes in critical section */

active [2] proctype process() {
    byte me = _pid;
    byte other = 1 - _pid;

    do
    :: /* Entry protocol */
       flag[me] = true;
       turn = other;
       (flag[other] == false || turn == me);

       /* Critical section */
       critical++;
       assert(critical == 1);  /* mutual exclusion */
       critical--;

       /* Exit protocol */
       flag[me] = false;
    od
}

/* LTL property: mutual exclusion always holds */
ltl mutex { [] (critical <= 1) }