diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2024-11-07
+        * Version bump (4.1). (#561)
+        * Reject duplicate externs in properties and theorems. (#536)
+        * Standardize changelog format. (#550)
+
 2024-09-07
         * Version bump (4.0). (#532)
         * Add support for array updates. (#36)
@@ -108,12 +113,12 @@
         * Completed the documentation. (#112)
 
 2020-05-07
-        * Version bump (3.2).
-        * Fixed the reverse order of triggers (#114).
-        * Update description, bug-reports, changelog fields in cabal file
-          (#116).
-        * Bump ghc-prim version bounds (#122).
+        * Version bump (3.2). (#65)
+        * Fixed the reverse order of triggers. (#114)
+        * Update description, bug-reports, changelog fields in cabal file.
+          (#116)
+        * Bump ghc-prim version bounds. (#122)
 
-2019-11-22 Ivan Perez <ivan.perez@nianet.org>
-        * Version bump (3.1).
-        * Remove ExternFun (#118).
+2019-11-22
+        * Version bump (3.1). (#46)
+        * Remove ExternFun. (#118)
diff --git a/copilot-language.cabal b/copilot-language.cabal
--- a/copilot-language.cabal
+++ b/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             4.0
+version:             4.1
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -42,9 +42,9 @@
                , data-reify            >= 0.6  && < 0.7
                , mtl                   >= 2.0  && < 3
 
-               , copilot-core          >= 4.0 && < 4.1
-               , copilot-interpreter   >= 4.0 && < 4.1
-               , copilot-theorem       >= 4.0 && < 4.1
+               , copilot-core          >= 4.1 && < 4.2
+               , copilot-interpreter   >= 4.1 && < 4.2
+               , copilot-theorem       >= 4.1 && < 4.2
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/src/Copilot/Language/Analyze.hs b/src/Copilot/Language/Analyze.hs
--- a/src/Copilot/Language/Analyze.hs
+++ b/src/Copilot/Language/Analyze.hs
@@ -17,6 +17,7 @@
 import Copilot.Language.Stream (Stream (..))
 import Copilot.Language.Spec
 import Copilot.Language.Error (badUsage)
+import Copilot.Theorem.Prove (UProof)
 
 import Data.List (groupBy)
 import Data.IORef
@@ -268,10 +269,16 @@
 -- | Obtain all the externs in a specification.
 specExts :: IORef Env -> Spec' a -> IO ExternEnv
 specExts refStreams spec = do
-  env <- foldM triggerExts
-           (ExternEnv [] [] [] [])
-           (triggers $ runSpec spec)
-  foldM observerExts env (observers $ runSpec spec)
+  env0 <- foldM triggerExts
+            (ExternEnv [] [] [] [])
+            (triggers $ runSpec spec)
+  env1 <- foldM observerExts
+            env0
+            (observers $ runSpec spec)
+  env2 <- foldM propertyExts
+            env1
+            (properties $ runSpec spec)
+  foldM theoremExts env2 (theorems $ runSpec spec)
 
   where
   observerExts :: ExternEnv -> Observer -> IO ExternEnv
@@ -282,6 +289,12 @@
     env' <- collectExts refStreams guard env
     foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')
           env' args
+
+  propertyExts :: ExternEnv -> Property -> IO ExternEnv
+  propertyExts env (Property _ stream) = collectExts refStreams stream env
+
+  theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv
+  theoremExts env (p, _) = propertyExts env p
 
 -- | Obtain all the externs in a stream.
 collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv