Lesson 265
Formal Verification
Hoare Logic · Model Checking · SAT/SMT
1:00How to prove programs correct for every possible input using Hoare logic, loop invariants, model checking, and SAT/SMT solvers — and why testing alone can never be enough.
By the end, you can
- Explain why testing cannot prove the absence of bugs and what formal verification does differently.
- Read and write a Hoare triple, identifying precondition, command, and postcondition.
- Apply the weakest-precondition assignment rule to derive a precondition from a postcondition.
- State the three obligations of a loop invariant proof and verify them for a simple loop.
- Describe how model checking works, what a counterexample trace is, and why state explosion is the central challenge.
- Distinguish a SAT solver from an SMT solver and explain the role each plays in verification tools.
- Name at least two real systems verified in production and identify which tool was used.
- Articulate the three fundamental limits of formal verification and why we still need testing.
Up next in Advanced Algorithms, Math & PL Theory
