Formal Verification for Working Software Engineers

From First Principles to Production-Grade Verified Systems

Introduction: Why Testing Is Not Enough

1. A History of Missed Bugs
2. What Formal Verification Actually Means
3. The Spectrum from Testing to Proofs
4. How This Book Is Structured

Chapter 1: Properties, Specifications, and Invariants

1. From Requirements to Precise Properties
2. Preconditions and Postconditions: Contracts for Code
3. Invariants: What Must Always Be True
4. Assertions as Lightweight Verification
5. State Machines and Behavioral Models
6. Designing Specifications That Are Checkable
7. Summary

Chapter 2: Logic and Mathematics for Verification

1. Propositional Logic: Truth Tables and Equivalences
2. Predicate Logic: Quantifiers and Properties Over Data
3. Sets, Relations, and Functions as Specification Tools
4. Boolean Algebra for Software Engineers
5. Induction: Proving Things About Arbitrary Inputs
6. Proof Techniques: Direct, Contradiction, Cases
7. Summary

Chapter 3: Hoare Logic and Program Correctness

1. Hoare Triples: The Language of Partial Correctness
2. Rules of Inference for Imperative Programs
3. P’ → P, {P} C {Q}, Q → Q’
4. Weakest Preconditions: Reasoning Backwards
5. Operational Semantics: Defining What Programs Mean
6. Sequencing: ⟨C1, σ⟩ ⇓ σ’, ⟨C2, σ’⟩ ⇓ σ’’
7. Total vs Partial Correctness and Termination
8. Proof Trees for Real Code
9. Summary

Chapter 4: Property-Based Testing as a Bridge to Formal Reasoning

1. From Example Tests to Universal Properties
2. QuickCheck, Hypothesis, and Property Frameworks
3. Shrinking Counterexamples: Learning from Failure
4. Invariants as Testable Properties
5. When Property Testing Succeeds and Fails
6. The Path from Properties to Proofs
7. Summary

Chapter 5: SAT Solvers and Boolean Reasoning

1. The Satisfiability Problem and Its Ubiquity
2. Conjunctive Normal Form: Encoding Problems as Logic
3. How SAT Solvers Work: DPLL and CDCL
4. Using SAT Solvers in Practice: MiniSat, Z3
5. Encoding Real Constraints for SAT
6. Limits of Pure Boolean Reasoning
7. Summary

Chapter 6: SMT Solvers and Constraint Solving

1. From SAT to SMT: Adding Theories
2. Core Theories: Arithmetic, Arrays, Bitvectors, Strings
3. Z3 and Other Major SMT Solvers
4. Encoding Programs as Constraints
5. Solver-Aided Programming Patterns
6. Interpreting Sat/Unsat and Models
7. Summary

Chapter 7: Symbolic Execution and Path Analysis

1. Symbolic Values and Path Conditions
2. Exploring Branches Systematically
3. Concolic Execution: Mixing Concrete and Symbolic
4. Bounded Model Checking via Symbolic Execution
5. Tools: KLEE, angr, CBMC
6. Path Explosion and Practical Mitigations
7. Summary

Chapter 8: Abstract Interpretation and Static Analysis

1. The Idea of Abstraction: Precision vs Soundness
2. Lattices and Fixpoints Made Intuitive
3. Common Analyses: Nullability, Ranges, Taint
4. Frama-C and the WP Plugin
5. SPARK/Ada for Safety-Critical Code
6. Trade-offs Between Soundness and Scalability
7. Summary

Chapter 9: Model Checking and Temporal Logic

1. State Spaces and Transition Systems
2. Linear-Time vs Branching-Time Temporal Logic
3. LTL and CTL: Specifying Behavioral Properties
4. How Model Checkers Explore State Spaces
5. TLA+ for Distributed Systems Design
6. State Explosion and Symmetry Breaking
7. Summary

Chapter 10: Deductive Verification with Contracts and Annotations

1. The Deductive Verification Pipeline
2. Dafny: Syntax, Contracts, and Automation
3. Loop Invariants and Recursive Functions
4. Framing Conditions and Modularity
5. Verus and Rust Verification
6. Debugging Failed Proofs
7. Summary

Chapter 11: Separation Logic and Memory Reasoning

1. The Problem of Shared Mutable State
2. Separating Conjunctions and Spatial Reasoning
3. Points-to Assertions and Heap Predicates
4. Verifying Pointer Manipulation
5. Prusti, Creusot, and Rust Verification
6. Concurrent Separation Logic Basics
7. Summary

Chapter 12: Concurrent Program Verification

1. What Goes Wrong in Concurrent Code
2. Linearizability and Atomicity Specifications
3. Race Detection vs Race Proofs
4. Lock-Based Reasoning and Ownership
5. Verifying Concurrent Data Structures
6. Tools: IronFleet, F*, Viper
7. Summary

Chapter 13: Distributed Systems and Protocol Verification

1. The Unique Challenges of Distributed Verification
2. Specifying Consensus and Replication
3. Alloy for Lightweight Structural Analysis
4. Verifying Paxos, Raft, and CRDTs
5. Handling Timeouts, Failures, and Network Partitions
6. IronFleet: Verified End-to-End Distributed Systems
7. Summary

Chapter 14: Theorem Proving with Proof Assistants

1. When You Need a Proof Assistant
2. Dependent Types and Propositions-as-Types
3. Interactive Proof Development in Lean
4. Tactics, Automation, and Proof Terms
5. Coq/Rocq for Certified Software
6. Isabelle/HOL for Large-Scale Verification
7. Summary

Chapter 15: Verified Compilers and Systems Software

1. Why Verify Compilers? The CompCert Story
2. Verified Operating System Kernels (seL4, Fuchsia)
3. Cryptographic Implementations in F* and Others
4. Proof-Carrying Code and Capabilities
5. Smart Contract Verification on Blockchains
6. Lessons from Million-Line Verified Systems
7. Summary

Chapter 16: Engineering Practice — Adoption, Workflows, and Culture

1. Choosing What to Verify: Risk vs Effort
2. The Trusted Computing Base and Its Limits
3. Integrating Verification into CI Pipelines
4. Specification Review and Proof Maintenance
5. Combining Verification with Testing and Fuzzing
6. Introducing Formal Methods to Engineering Teams
7. Summary

Major Case Study: From Tests to Verified System

1. The Component: Requirements and Initial Implementation
2. Baseline Testing and Its Blind Spots
3. Adding Property-Based Testing
4. SMT-Based Contract Checking with Dafny
5. Model Checking the State Machine in TLA+
6. Machine-Checked Proofs for Critical Properties
7. CI Integration and Regression Guarantees
8. What We Learned: Costs, Benefits, Trade-offs
9. Summary

Conclusion: The Future of Verified Software Engineering

1. Where Formal Verification Has Succeeded
2. AI and Language Models in Verification Workflows
3. The Remaining Gaps Between Research and Practice
4. A Pragmatic Philosophy for Verified Software
5. Getting Started Tomorrow

References