Prior reading: What Are Formal Methods?

What Is Model Checking?

Given a model of a system and a property expressed in formal logic, model checking exhaustively verifies whether the property holds in all reachable states.

Temporal Logic Crash Course

  • LTL (Linear Temporal Logic): "Eventually the system reaches a safe state." $\Diamond \text{safe}$
  • CTL (Computation Tree Logic): "On all paths, the system never enters an unsafe state." $\forall\Box \neg \text{unsafe}$
  • These let you express liveness, safety, and fairness properties.

Classical Model Checking

Works brilliantly for finite-state systems: protocols, hardware, control software. Tools like SPIN, NuSMV, and PRISM are mature.

The AI Challenge

Neural networks don't have discrete states in the traditional sense. The "state space" is continuous and astronomically large. Approaches:

  • Abstracting neural network behavior into finite models
  • Hybrid systems: Combine discrete control logic with continuous NN components
  • Runtime verification: Check properties online as the system runs, rather than exhaustively ahead of time

Why Specification Matters

Model checking is only as good as your spec. If you can't formally state what "safe" or "aligned" means, you can't check it. This leads directly to the specification problem.