diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 51a5dea..053bb63 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -15,8 +15,8 @@ jobs:
           - "4.6.0"
           - "4.7.0"
           - "4.8.0"
-          - "4.9.0-rc1"
-          - "nightly-2024-06-12"
+          - "4.9.0"
+          - "nightly-2024-07-12"
         platform:
           - os: ubuntu-latest
             installer: |
@@ -24,7 +24,7 @@ jobs:
         # Mac runners are rare and expensive, so spot-check that the
         # subprocess support seems OK but be less thorough
         include:
-          - toolchain: "4.8.0"
+          - toolchain: "4.9.0"
             platform:
               os: macos-latest
               installer: |
diff --git a/.github/workflows/formalities.yml b/.github/workflows/formalities.yml
new file mode 100644
index 0000000..bd35c0d
--- /dev/null
+++ b/.github/workflows/formalities.yml
@@ -0,0 +1,28 @@
+on:
+  push:
+  pull_request:
+
+name: Formalities
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Don't 'import Lean', use precise imports
+        if: always()
+        run: |
+          ! (find . -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+
+      - name: Verify .lean files start with a copyright header.
+        run: |
+          FILES=$(find ./src ./demo ./demo-toml -not -path '*/.lake/*' -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
+          if [ -n "$FILES" ]; then
+            echo "Found .lean files which do not have a copyright header:"
+            echo "$FILES"
+            exit 1
+          else
+            echo "All copyright headers present."
+          fi
diff --git a/Extract.lean b/Extract.lean
index 8cd905d..86d8c91 100644
--- a/Extract.lean
+++ b/Extract.lean
@@ -1,4 +1,8 @@
-import Lean
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import SubVerso.Examples.Env
 
 open Lean
diff --git a/demo-toml/Demo.lean b/demo-toml/Demo.lean
index 2e70ebc..4722907 100644
--- a/demo-toml/Demo.lean
+++ b/demo-toml/Demo.lean
@@ -1,5 +1,8 @@
--- This module serves as the root of the `Demo` library.
--- Import modules here that should be built as part of the library.
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo».Basic
 
 import SubVerso.Examples
diff --git a/demo-toml/Demo/Basic.lean b/demo-toml/Demo/Basic.lean
index e99d3a6..a6c7968 100644
--- a/demo-toml/Demo/Basic.lean
+++ b/demo-toml/Demo/Basic.lean
@@ -1 +1,6 @@
-def hello := "world"
\ No newline at end of file
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+def hello := "world"
diff --git a/demo-toml/Main.lean b/demo-toml/Main.lean
index 4a6d743..e2bab30 100644
--- a/demo-toml/Main.lean
+++ b/demo-toml/Main.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo»
 
 def main : IO Unit :=
diff --git a/demo/Demo.lean b/demo/Demo.lean
index ff48186..ea368d6 100644
--- a/demo/Demo.lean
+++ b/demo/Demo.lean
@@ -1,5 +1,8 @@
--- This module serves as the root of the `Demo` library.
--- Import modules here that should be built as part of the library.
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo».Basic
 
 import SubVerso.Examples
diff --git a/demo/Demo/Basic.lean b/demo/Demo/Basic.lean
index e99d3a6..a6c7968 100644
--- a/demo/Demo/Basic.lean
+++ b/demo/Demo/Basic.lean
@@ -1 +1,6 @@
-def hello := "world"
\ No newline at end of file
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+def hello := "world"
diff --git a/demo/Main.lean b/demo/Main.lean
index 4a6d743..e2bab30 100644
--- a/demo/Main.lean
+++ b/demo/Main.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo»
 
 def main : IO Unit :=
diff --git a/demo/lakefile.lean b/demo/lakefile.lean
index 59cf3c0..f79bf30 100644
--- a/demo/lakefile.lean
+++ b/demo/lakefile.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import Lake
 open Lake DSL
 
diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
index 7e22a7b..50a4e0e 100644
--- a/src/compat/SubVerso/Compat.lean
+++ b/src/compat/SubVerso/Compat.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import Lean.Elab
 
 open Lean Elab Term
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
index 61922d8..2f2a748 100644
--- a/src/examples/SubVerso/Examples.lean
+++ b/src/examples/SubVerso/Examples.lean
@@ -1,7 +1,13 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import Lean.Environment
 import SubVerso.Highlighting
 import SubVerso.Compat
 import SubVerso.Examples.Env
-import Lean.Environment
+
 
 namespace SubVerso.Examples
 
@@ -284,7 +290,7 @@ elab_rules : command
     let addScope x := mkIdentFrom x (addMacroScope mod x.getId sc)
     let declName ← match sigName with
       | `(Lean.Parser.Command.declId|$x:ident) => pure x
-      | `(Lean.Parser.Command.declId|$x:ident.{$u:ident,*}) => pure x
+      | `(Lean.Parser.Command.declId|$x:ident.{$_u:ident,*}) => pure x
       | _ => throwErrorAt sigName "Unexpected format of name: {sigName}"
     let target ← liftTermElabM <| Compat.realizeNameNoOverloads declName
     let noClash ← match sigName with
diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean
index 17f8705..1dd6adf 100644
--- a/src/examples/SubVerso/Examples/Env.lean
+++ b/src/examples/SubVerso/Examples/Env.lean
@@ -1,4 +1,8 @@
-import Lean
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import SubVerso.Highlighting
 
 open Lean
diff --git a/src/highlighting/SubVerso/Highlighting.lean b/src/highlighting/SubVerso/Highlighting.lean
index 0a0ae0d..93169f5 100644
--- a/src/highlighting/SubVerso/Highlighting.lean
+++ b/src/highlighting/SubVerso/Highlighting.lean
@@ -1,2 +1,7 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import SubVerso.Highlighting.Highlighted
 import SubVerso.Highlighting.Code
diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean
index f2e8342..c2a7007 100644
--- a/src/highlighting/SubVerso/Highlighting/Code.lean
+++ b/src/highlighting/SubVerso/Highlighting/Code.lean
@@ -1,6 +1,12 @@
-import Lean
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import Lean.Widget.InteractiveCode
 import Lean.Widget.TaggedText
 
+
 import SubVerso.Compat
 import SubVerso.Highlighting.Highlighted
 
diff --git a/src/highlighting/SubVerso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
index 2b8af2c..12ef238 100644
--- a/src/highlighting/SubVerso/Highlighting/Highlighted.lean
+++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
@@ -1,4 +1,11 @@
-import Lean
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import Lean.Data.Json
+import Lean.Expr
+import Lean.SubExpr -- for the To/FromJSON FVarId instances
 
 open Lean