--- name: formal-verification-guide-e6f068281d79 description: "Formal methods, theorem proving, and model checking for CS research" metadata: openclaw: emoji: "✅" category: "domains" subcategory: "cs" keywords: ["formal-verification", "theorem-proving", "model-checking", "tla-plus", "coq", "isabelle"] source: "wentor" --- # Formal Verification Guide A skill for applying formal methods to verify software and hardware correctness. Covers model checking, interactive theorem proving, specification languages, and practical verification workflows used in systems and programming language research. ## Verification Approaches Overview ### Methods Comparison | Approach | Technique | Strengths | Limitations | |----------|-----------|-----------|-------------| | Model checking | Exhaustive state exploration | Fully automatic, produces counterexamples | State space explosion | | Theorem proving | Interactive proof construction | Handles infinite state | Requires expert effort | | Abstract interpretation | Sound static analysis | Automatic, scales well | May report false positives | | SMT solving | Constraint satisfiability | Powerful automation | Limited to decidable theories | | Runtime verification | Execution monitoring | Low barrier, practical | Only checks observed runs | ## TLA+ Specification ### Specifying Distributed Protocols TLA+ is the standard specification language for distributed systems: ```tla --------------------------- 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 == <> 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 <> \* TM receives a Prepared message from RM r TMRcvPrepared(r) == /\ tmState = "init" /\ [type |-> "Prepared", rm |-> r] \in msgs /\ tmPrepared' = tmPrepared \union {r} /\ UNCHANGED <> \* TM commits (all RMs have prepared) TMCommit == /\ tmState = "init" /\ tmPrepared = RM /\ tmState' = "committed" /\ msgs' = msgs \union {[type |-> "Commit"]} /\ UNCHANGED <> \* Safety property: No RM commits unless TM has committed Consistency == \A r \in RM : rmState[r] = "committed" => tmState = "committed" ======================================================================== ``` ### Running the TLC Model Checker ```bash # 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) ``` ## Interactive Theorem Proving ### Coq Proof Assistant ```coq (* 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. ``` ### Isabelle/HOL ```isabelle 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 ``` ## SMT Solving ### Z3 for Program Verification ```python 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} ``` ## Model Checking with SPIN ### Promela Specification ```promela /* 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) } ``` ## Verification Workflow ### Practical Verification Strategy 1. **Specify**: Write a formal specification of the desired property 2. **Model**: Create an abstract model of the system 3. **Verify**: Run model checker or construct proof 4. **Refine**: If counterexample found, fix the design or refine the model 5. **Extract**: Generate verified code from the proof (Coq extraction, Isabelle code generation) ### Common Properties to Verify | Property Type | Example | Specification Pattern | |--------------|---------|----------------------| | Safety | "No two processes in critical section" | `[] (count <= 1)` | | Liveness | "Every request is eventually served" | `[] (request -> <> response)` | | Deadlock freedom | "System always has an enabled transition" | `[] <> enabled` | | Termination | "Program always halts" | Well-founded ordering | ## Tools and Resources - **TLA+ Toolbox**: IDE for TLA+ with integrated TLC model checker - **Coq**: Interactive theorem prover with program extraction - **Isabelle/HOL**: Higher-order logic prover with Sledgehammer automation - **Z3 / CVC5**: SMT solvers for automated reasoning - **SPIN**: Model checker for concurrent systems (Promela) - **CBMC**: Bounded model checker for C programs - **Dafny**: Verification-aware programming language (Microsoft) - **Lean 4**: Modern theorem prover and programming language --- Source attribution: wentorai Original project: https://github.com/wentorai/research-plugins/blob/bf44b3cd617fa94c8a1b254c5d1987142ca3d631/skills/domains/cs/formal-verification-guide/SKILL.md License: MIT License information: https://opensource.org/license/mit Original upstream instructions; downloaded from Mega AI Hub. ## Upstream license notice MIT License Copyright (c) 2026 Wentor AI Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. # Mega AI Hub resource metadata Creator / publisher: wentorai Original project: https://github.com/wentorai/research-plugins/blob/bf44b3cd617fa94c8a1b254c5d1987142ca3d631/skills/domains/cs/formal-verification-guide/SKILL.md Attribution basis: Source repository record Fields of work: Data & Analytics, Development & Engineering, Education & Research Roles: Data Scientist, ML / AI Engineer, Researcher Specialties: API Tools: Coq, Tla+ Country applicability: Country not specified Classification basis: Source catalog labels Instruction SHA-256: c806ce7a760ab26314c5c1b5988858e3f88dbedc50dae8f694a6b297d005c9d0