diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,40 +1,50 @@
+2025-07-07
+        * Version bump (4.5). (#642)
+        * Include `copilot-verifier` in mainline `copilot` repo. (#622)
+
 2025-05-08
-        * Version bump (4.4). (#85)
+        * Version bump (4.4). (copilot-verifier#85)
 
 2025-03-10
-        * Version bump (4.3). (#82)
-        * Add `smtSolver` option to `VerifierOptions`. (#78)
-        * Add `smtFloatMode` option to `VerifierOptions`. (#79)
+        * Version bump (4.3). (copilot-verifier#82)
+        * Add `smtSolver` option to `VerifierOptions`. (copilot-verifier#78)
+        * Add `smtFloatMode` option to `VerifierOptions`. (copilot-verifier#79)
 
 2025-01-20
-        * Version bump (4.2). (#76)
-        * Reject specs that use multiple triggers with the same name. (#74)
+        * Version bump (4.2). (copilot-verifier#76)
+        * Reject specs that use multiple triggers with the same name.
+          (copilot-verifier#74)
 
 2024-11-08
-        * Version bump (4.1). (#72)
+        * Version bump (4.1). (copilot-verifier#72)
 
 2024-09-09
-        * Version bump (4.0). (#69)
-        * Support verifying programs that use array updates. (#63)
-        * Support verifying programs that use struct updates. (#57)
+        * Version bump (4.0). (copilot-verifier#69)
+        * Support verifying programs that use array updates.
+          (copilot-verifier#63)
+        * Support verifying programs that use struct updates.
+          (copilot-verifier#57)
 
 2024-08-03
-        * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)
-        * Support GHC 9.4 through 9.8. (#65)
+        * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`.
+          (copilot-verifier#64)
+        * Support GHC 9.4 through 9.8. (copilot-verifier#65)
 
 2024-07-30
         * When using `Noisy` verbosity, always log proof goals related to the
-          core correspondence proof, even if the goals are trivial. (#51)
+          core correspondence proof, even if the goals are trivial.
+          (copilot-verifier#51)
         * When using `Noisy` verbosity, log more information about which proof
-          goals arise before or after calling the `step()` function. (#52)
+          goals arise before or after calling the `step()` function.
+          (copilot-verifier#52)
 
 2024-07-11
-        * Version bump (3.20). (#58)
+        * Version bump (3.20). (copilot-verifier#58)
 
 2024-03-08
-        * Version bump (3.19). (#53)
+        * Version bump (3.19). (copilot-verifier#53)
         * Provide more detailed feedback upon a successful run of the verifier.
-        * Make the examples build with Copilot 3.19. (#53)
+        * Make the examples build with Copilot 3.19. (copilot-verifier#53)
 
 2024-02-06
         * Initial release of `copilot-verifier`.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/copilot-verifier.cabal b/copilot-verifier.cabal
--- a/copilot-verifier.cabal
+++ b/copilot-verifier.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          copilot-verifier
-Version:       4.4
+Version:       4.5
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com
 Copyright:     (c) Galois, Inc 2021-2024
@@ -45,9 +45,9 @@
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot-c99 >= 4.4 && < 4.5,
-    copilot-core >= 4.4 && < 4.5,
-    copilot-theorem >= 4.4 && < 4.5,
+    copilot-c99 >= 4.5 && < 4.6,
+    copilot-core >= 4.5 && < 4.6,
+    copilot-theorem >= 4.5 && < 4.6,
     crucible >= 0.7.1 && < 0.8,
     crucible-llvm >= 0.7 && < 0.8,
     crux >= 0.7.1 && < 0.8,
@@ -80,10 +80,10 @@
   hs-source-dirs: examples
   build-depends:
     case-insensitive,
-    copilot >= 4.4 && < 4.5,
-    copilot-language >= 4.4 && < 4.5,
-    copilot-libraries >= 4.4 && < 4.5,
-    copilot-prettyprinter >= 4.4 && < 4.5,
+    copilot >= 4.5 && < 4.6,
+    copilot-language >= 4.5 && < 4.6,
+    copilot-libraries >= 4.5 && < 4.6,
+    copilot-prettyprinter >= 4.5 && < 4.6,
     copilot-verifier
   exposed-modules:
     Copilot.Verifier.Examples