diff --git a/Frap.v b/Frap.v
index b95b0d6..f54b292 100644
--- a/Frap.v
+++ b/Frap.v
@@ -1,5 +1,5 @@
-Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool.
-Export String Arith Sets Relations Map Var Invariant Bool.
+Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
+Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
 Require Import List.
 Export List ListNotations.
 Open Scope string_scope.
@@ -89,3 +89,40 @@ Export Frap.Map.
 Ltac maps_equal := Frap.Map.M.maps_equal; simplify.
 
 Ltac first_order := firstorder idtac.
+
+
+(** * Model checking *)
+
+Ltac model_check_done :=
+  apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
+  repeat match goal with
+         | [ H : _ |- _ ] => invert H
+         end; simplify; equality.
+
+Ltac singletoner :=
+  repeat match goal with
+         | _ => apply singleton_in
+         | [ |- (_ \cup _) _ ] => apply singleton_in_other
+         end.
+
+Ltac model_check_step :=
+  eapply MscStep; [
+    repeat ((apply oneStepClosure_empty; simplify)
+            || (apply oneStepClosure_split; [ simplify;
+                                              repeat match goal with
+                                                     | [ H : _ |- _ ] => invert H; try congruence
+                                                     end; solve [ singletoner ] | ]))
+  | simplify ].
+
+Ltac model_check_steps1 := model_check_done || model_check_step.
+Ltac model_check_steps := repeat model_check_steps1.
+
+Ltac model_check_finish := simplify; propositional; subst; simplify; equality.
+
+Ltac model_check_infer :=
+  apply multiStepClosure_ok; simplify; model_check_steps.
+
+Ltac model_check_find_invariant :=
+  simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
+
+Ltac model_check := model_check_find_invariant; model_check_finish.
diff --git a/ModelCheck.v b/ModelCheck.v
new file mode 100644
index 0000000..f7a25ab
--- /dev/null
+++ b/ModelCheck.v
@@ -0,0 +1,97 @@
+Require Import Invariant Sets.
+
+Definition oneStepClosure_current {state} (sys : trsys state)
+           (invariant1 invariant2 : state -> Prop) :=
+  forall st, invariant1 st
+             -> invariant2 st.
+
+Definition oneStepClosure_new {state} (sys : trsys state)
+           (invariant1 invariant2 : state -> Prop) :=
+  forall st st', invariant1 st
+                 -> sys.(Step) st st'
+                 -> invariant2 st'.
+
+Definition oneStepClosure {state} (sys : trsys state)
+           (invariant1 invariant2 : state -> Prop) :=
+  oneStepClosure_current sys invariant1 invariant2
+  /\ oneStepClosure_new sys invariant1 invariant2.
+
+Theorem prove_oneStepClosure : forall state (sys : trsys state) (inv1 inv2 : state -> Prop),
+  (forall st, inv1 st -> inv2 st)
+  -> (forall st st', inv1 st -> sys.(Step) st st' -> inv2 st')
+  -> oneStepClosure sys inv1 inv2.
+Proof.
+  unfold oneStepClosure; tauto.
+Qed.
+
+Theorem oneStepClosure_done : forall state (sys : trsys state) (invariant : state -> Prop),
+  (forall st, sys.(Initial) st -> invariant st)
+  -> oneStepClosure sys invariant invariant
+  -> invariantFor sys invariant.
+Proof.
+  unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new.
+  intuition eauto using invariant_induction.
+Qed.
+
+Inductive multiStepClosure {state} (sys : trsys state)
+  : (state -> Prop) -> (state -> Prop) -> Prop :=
+| MscDone : forall inv,
+    oneStepClosure sys inv inv
+    -> multiStepClosure sys inv inv
+| MscStep : forall inv inv' inv'',
+    oneStepClosure sys inv inv'
+    -> multiStepClosure sys inv' inv''
+    -> multiStepClosure sys inv inv''.
+
+Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv inv' : state -> Prop),
+  multiStepClosure sys inv inv'
+  -> (forall st, sys.(Initial) st -> inv st)
+  -> invariantFor sys inv'.
+Proof.
+  induction 1; simpl; intuition eauto using oneStepClosure_done.
+
+  unfold oneStepClosure, oneStepClosure_current in *.
+  intuition eauto.
+Qed.
+
+Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> Prop),
+  multiStepClosure sys sys.(Initial) inv
+  -> invariantFor sys inv.
+Proof.
+  eauto using multiStepClosure_ok'.
+Qed.
+
+Theorem oneStepClosure_empty : forall state (sys : trsys state),
+  oneStepClosure sys (constant nil) (constant nil).
+Proof.
+  unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; intuition.
+Qed.
+
+Theorem oneStepClosure_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop),
+  (forall st', sys.(Step) st st' -> inv1 st')
+  -> oneStepClosure sys (constant sts) inv2
+  -> oneStepClosure sys (constant (st :: sts)) ({st} \cup inv1 \cup inv2).
+Proof.
+  unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; intuition.
+
+  inversion H0; subst.
+  unfold union; simpl; tauto.
+
+  unfold union; simpl; eauto.
+
+  unfold union in *; simpl in *.
+  intuition (subst; eauto).
+Qed.
+
+Theorem singleton_in : forall {A} (x : A) rest,
+  ({x} \cup rest) x.
+Proof.
+  unfold union; simpl; auto.
+Qed.
+
+Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
+  s2 x
+  -> (s1 \cup s2) x.
+Proof.
+  unfold union; simpl; auto.
+Qed.
diff --git a/ModelChecking.v b/ModelChecking.v
index 5b94ac2..04892cc 100644
--- a/ModelChecking.v
+++ b/ModelChecking.v
@@ -103,7 +103,7 @@ Proof.
 
   apply IHmultiStepClosure.
   simplify.
-  unfold oneStepClosure, oneStepClosure_current in *. (* <-- *)
+  unfold oneStepClosure, oneStepClosure_current in *.
   propositional.
   apply H3.
   apply H1.
diff --git a/README.md b/README.md
index 03306b3..bb043a9 100644
--- a/README.md
+++ b/README.md
@@ -9,3 +9,4 @@ Just run `make` here to build everything, including the book `frap.pdf` and the
 * Chapter 2: `BasicSyntax.v`
 * Chapter 3: `Interpreters.v`
 * Chapter 4: `TransitionSystems.v`
+* Chapter 5: `ModelChecking.v`
diff --git a/_CoqProject b/_CoqProject
index 76fa450..e6bdf5f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,7 @@ Var.v
 Sets.v
 Relations.v
 Invariant.v
+ModelCheck.v
 Frap.v
 BasicSyntax_template.v
 BasicSyntax.v