diff --git a/.claude/commands/formspec.check.8.md b/.claude/commands/formspec.check.8.md
index 500277f..9060ada 100644
--- a/.claude/commands/formspec.check.8.md
+++ b/.claude/commands/formspec.check.8.md
@@ -1,5 +1,6 @@
 ---
 description: Cross-artifact consistency check across all formspec artifacts
+argument-hint: [scope]
 allowed-tools: [Read, Glob, Grep, Bash, Task]
 ---
 
diff --git a/.claude/commands/formspec.formalize.2.md b/.claude/commands/formspec.formalize.2.md
index a4d20f5..a45376c 100644
--- a/.claude/commands/formspec.formalize.2.md
+++ b/.claude/commands/formspec.formalize.2.md
@@ -85,7 +85,10 @@ Every requirement from Phase 1 must appear in this table. If a requirement canno
 
 ## Phase 4 — Run TLC model checker
 
-Run:
+If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs, and skip to Phase 5.
+
+If the hook does not exist or fails, run TLC locally:
+
 ```bash
 tlc spec/formal/System.tla -config spec/formal/System.cfg -workers auto -metadir /tmp/tlc-states -cleanup
 ```
@@ -113,11 +116,7 @@ Parse the TLC output to determine:
 
 ### All properties pass
 
-If `spec/hooks/run-checks` exists and is executable, delegate TLC verification to it instead of running TLC locally (see `/formspec.init` for the hook interface). Present the returned results to the developer, including any dashboard URLs.
-
-If the hook does not exist or fails, run TLC locally as described in Phase 4.
-
-In either case, update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan.
+Update all statuses in `spec/formal/traceability.md` from `formalized` to `checked`. Report success with a summary of what was verified: number of properties checked, state space explored, time taken. Suggest proceeding with `/formspec.plan.4` to create an implementation plan.
 
 ### Meaning drift detected (Phase 2 issue)
 
diff --git a/.claude/commands/formspec.implement.6.md b/.claude/commands/formspec.implement.6.md
index 1bdf960..7a7ee9f 100644
--- a/.claude/commands/formspec.implement.6.md
+++ b/.claude/commands/formspec.implement.6.md
@@ -66,7 +66,9 @@ After unit tests pass, mark the task complete in `spec/tasks.md` (e.g., append `
 
 **e. Continue to next task**:
 
-After completing a task, if the next task's dependencies are all met, continue implementing it without stopping. Keep going until either:
+After completing a task, present a brief summary of what was implemented and the test results. Then ask the developer whether to continue to the next task or pause for review. If the developer chooses to continue (or has previously indicated they want uninterrupted execution), proceed to the next task whose dependencies are all met.
+
+Stop regardless of the developer's preference when:
 - A unit test failure or spec inconsistency requires developer input
 - A verification milestone is reached (all of its tasks are now complete)
 - No more tasks are ready (unmet dependencies)
diff --git a/.claude/commands/formspec.verify.3.md b/.claude/commands/formspec.verify.3.md
index a19354b..caeb654 100644
--- a/.claude/commands/formspec.verify.3.md
+++ b/.claude/commands/formspec.verify.3.md
@@ -1,5 +1,6 @@
 ---
 description: Run the TLC model checker on the formal specification
+argument-hint: [property-name]
 allowed-tools: [Read, Glob, Grep, Bash]
 ---
 
diff --git a/.config/emacs/init.el b/.config/emacs/init.el
index 38679d2..b457fe1 100644
--- a/.config/emacs/init.el
+++ b/.config/emacs/init.el
@@ -89,15 +89,19 @@
          )
   )
 
-(use-package diminish)
+(use-package diminish
+  :ensure t
+  )
 
 (use-package better-defaults
   :ensure (:repo "https://git.sr.ht/~technomancy/better-defaults"))
 
 (use-package treemacs-icons-dired
+  :ensure t
   :hook (dired-mode . treemacs-icons-dired-mode))
 
 (use-package dired-subtree
+  :ensure t
   :after dired
   :bind (:map dired-mode-map
               ("<tab>" . dired-subtree-toggle)
@@ -119,11 +123,14 @@
   :diminish undo-tree-mode
   )
 
-(use-package transient)
+(use-package transient
+  :ensure t
+  )
 
 (use-package cond-let
   :ensure (:repo "https://github.com/tarsius/cond-let"))
 (use-package magit
+  :ensure t
   :bind (("C-x g" . magit-status)
          ("C-x M-g" . magit-list-repositories))
   :init
@@ -134,6 +141,7 @@
      ("~/Projects/" . 1))))
 
 (use-package nyan-mode
+  :ensure t
   :init
   (nyan-mode 1)
   :custom
@@ -141,9 +149,11 @@
   (nyan-wavy-trail t))
 
 (use-package mozc
+  :ensure t
   :bind (("C-c m" . mozc-mode)))
 
 (use-package material-theme
+  :ensure t
   :config
   (load-theme 'material t))
 
@@ -155,6 +165,7 @@
          ("s-d" . windmove-right)))
 
 (use-package counsel
+  :ensure t
   :bind (("C-s" . swiper-isearch)
          ("M-x" . counsel-M-x)
          ("M-y" . counsel-yank-pop)
@@ -209,8 +220,11 @@
   ;; keep-sorted end
   )
 
-(use-package org-contrib)
+(use-package org-contrib
+  :ensure t
+  )
 (use-package org-contacts
+  :ensure t
   :after org-contrib)
 
 (use-package deflate
@@ -230,6 +244,7 @@
   )
 
 (use-package age
+  :ensure t
   :custom
   (age-default-identity "~/.age/key")
   (age-default-recipient "~/.age/key.pub")
@@ -238,6 +253,7 @@
 
 ;; EPUB reader
 (use-package nov
+  :ensure t
   :init
   (setq auto-mode-alist
         (map-merge 'list
@@ -246,13 +262,16 @@
   )
 
 (use-package company
+  :ensure t
   :config (global-company-mode)
   :diminish company-mode)
 
 (use-package apt-mode
+  :ensure t
   :disabled t)
 
 (use-package docker
+  :ensure t
   :bind ("C-c d" . docker)
   :custom
   (docker-command "podman")
@@ -261,10 +280,15 @@
      (:name "Name" :width 50 :template "{{ json .Name }}" :sort nil :format nil)
      (:name "Driver" :width 10 :template "{{ json .Driver }}" :sort nil :format nil))))
 
-(use-package iedit)
-(use-package wgrep)
+(use-package iedit
+  :ensure t
+  )
+(use-package wgrep
+  :ensure t
+  )
 
 (use-package apheleia
+  :ensure t
   :config
   (apheleia-global-mode)
   (setf (alist-get 'ruff-isort apheleia-formatters)
@@ -294,10 +318,14 @@
   )
 
 ;; Note: debugging Python in a virtualenv requires debugpy to be installed inside the venv
-(use-package dape)
+(use-package dape
+  :ensure t
+  )
 
 ;; Requires poetry to be installed
-(use-package poetry)
+(use-package poetry
+  :ensure t
+  )
 
 (defun load-python-env ()
   "Set up the Python IDE in the current project."
@@ -308,6 +336,7 @@
       (eglot-ensure))))
 
 (use-package python
+  :ensure t
   :bind (:map python-ts-mode-map
               ("C-c C-p" . nil)
               ("C-c C-l" . nil)
@@ -321,6 +350,7 @@
 
 ;; Jupyter notebook integration
 (use-package ein
+  :ensure t
   :bind (("C-z j" . ein:run)
          :map ein:notebook-mode-map
          ("C-c C-x k" . ein:notebook-switch-kernel))
@@ -334,10 +364,12 @@
   )
 
 (use-package direnv
+  :ensure t
   :config
   (direnv-mode))
 
 (use-package rustic
+  :ensure t
   :custom
   (rustic-lsp-client 'eglot)
   )
@@ -378,6 +410,7 @@
     :models (enrich-ollama-models (list-ollama-models) gptel--local-models)))
 
 (use-package gptel
+  :ensure t
   :hook
   ;; keep-sorted start
   (gptel-mode . gptel-highlight-mode)
@@ -402,9 +435,12 @@
   (generate-ollama-declaration)
   )
 
-(use-package power-mode)
+(use-package power-mode
+  :ensure t
+  )
 
 (use-package emms
+  :ensure t
   :config
   (require 'emms-setup)
   (emms-all)
@@ -425,4 +461,5 @@
         (qrencode--encode-to-buffer url)))))
 
 (use-package qrencode
+  :ensure t
   :bind (("C-z q" . my-qr-selection)))