diff --git a/.vscode/vdmignore b/.vscode/vdmignore
new file mode 100644
index 0000000..55bdc3d
--- /dev/null
+++ b/.vscode/vdmignore
@@ -0,0 +1,2 @@
+doc/
+pub/
diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl
new file mode 100644
index 0000000..134d3e1
--- /dev/null
+++ b/formal/checklist.vdmsl
@@ -0,0 +1,25 @@
+module Checklist
+exports all
+definitions
+
+values
+
+types
+
+    String = seq of char;
+
+    -- Item of a checklist, e.g. Landing gear down
+    Item ::
+            todo : String
+            checked : bool;
+
+    -- A section of a checklist, e.g. Landing Checklist
+    Section = seq of Item;
+
+    -- Full checklist, e.g. Startup, Descent, Landing Checklist
+    Checklist = seq of Section;
+
+functions
+
+end Checklist
+