diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG
index 48f275cf7..00f705df8 100644
--- a/copilot-c99/CHANGELOG
+++ b/copilot-c99/CHANGELOG
@@ -1,3 +1,6 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+
 2025-03-07
         * Version bump (4.3). (#604)
 
diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal
index 48fc6aa36..dabf04bf0 100644
--- a/copilot-c99/copilot-c99.cabal
+++ b/copilot-c99/copilot-c99.cabal
@@ -1,6 +1,6 @@
 cabal-version             : >= 1.10
 name                      : copilot-c99
-version                   : 4.3
+version                   : 4.4
 synopsis                  : A compiler for Copilot targeting C99.
 description               :
   This package is a back-end from Copilot to C.
@@ -45,7 +45,7 @@ library
                           , mtl                 >= 2.2 && < 2.4
                           , pretty              >= 1.1 && < 1.2
 
-                          , copilot-core        >= 4.3   && < 4.4
+                          , copilot-core        >= 4.4   && < 4.5
                           , language-c99        >= 0.2.0 && < 0.3
                           , language-c99-simple >= 0.3   && < 0.4
 
diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG
index 371c8c2d9..4a0902c21 100644
--- a/copilot-core/CHANGELOG
+++ b/copilot-core/CHANGELOG
@@ -1,3 +1,7 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+        * Remove deprecated Copilot.Core.Type.uTypeType. (#615)
+
 2025-03-07
         * Version bump (4.3). (#604)
         * Fix typo in documentation. (#587)
diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index 1140f129e..daab8383b 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             4.3
+version:             4.4
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs
index 8d54c82f3..b290810c2 100644
--- a/copilot-core/src/Copilot/Core/Type.hs
+++ b/copilot-core/src/Copilot/Core/Type.hs
@@ -289,8 +289,7 @@ instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
   simpleType (Array t) = SArray t
 
 -- | A untyped type (no phantom type).
-data UType = forall a . Typeable a => UType { uTypeType :: Type a }
-{-# DEPRECATED uTypeType "This field is deprecated in Copilot 4.1. Use pattern matching instead." #-}
+data UType = forall a . Typeable a => UType (Type a)
 
 instance Eq UType where
   UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2
diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG
index 924fa7436..c5f4894c8 100644
--- a/copilot-interpreter/CHANGELOG
+++ b/copilot-interpreter/CHANGELOG
@@ -1,3 +1,6 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+
 2025-03-07
         * Version bump (4.3). (#604)
 
diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal
index 835f27106..d5b679829 100644
--- a/copilot-interpreter/copilot-interpreter.cabal
+++ b/copilot-interpreter/copilot-interpreter.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-interpreter
-version:             4.3
+version:             4.4
 synopsis:            Interpreter for Copilot.
 description:
   Interpreter for Copilot.
@@ -44,7 +44,7 @@ library
     base       >= 4.9 && < 5,
     pretty     >= 1.0 && < 1.2,
 
-    copilot-core >= 4.3 && < 4.4
+    copilot-core >= 4.4 && < 4.5
 
   exposed-modules:
 
diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG
index 2f729caac..fc28f01f1 100644
--- a/copilot-language/CHANGELOG
+++ b/copilot-language/CHANGELOG
@@ -1,3 +1,6 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+
 2025-03-07
         * Version bump (4.3). (#604)
         * Fix typo in documentation. (#587)
diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal
index 53c981618..87d54101d 100644
--- a/copilot-language/copilot-language.cabal
+++ b/copilot-language/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             4.3
+version:             4.4
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -42,9 +42,9 @@ library
                , data-reify            >= 0.6  && < 0.7
                , mtl                   >= 2.0  && < 3
 
-               , copilot-core          >= 4.3 && < 4.4
-               , copilot-interpreter   >= 4.3 && < 4.4
-               , copilot-theorem       >= 4.3 && < 4.4
+               , copilot-core          >= 4.4 && < 4.5
+               , copilot-interpreter   >= 4.4 && < 4.5
+               , copilot-theorem       >= 4.4 && < 4.5
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG
index 228e37a5d..a0c598f54 100644
--- a/copilot-libraries/CHANGELOG
+++ b/copilot-libraries/CHANGELOG
@@ -1,3 +1,6 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+
 2025-03-07
         * Version bump (4.3). (#604)
         * Remove deprecated function Copilot.Library.Utils.(!!). (#599)
diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal
index 737a590e7..078d009fd 100644
--- a/copilot-libraries/copilot-libraries.cabal
+++ b/copilot-libraries/copilot-libraries.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-libraries
-version:             4.3
+version:             4.4
 synopsis:            Libraries for the Copilot language.
 description:
   Libraries for the Copilot language.
@@ -41,7 +41,7 @@ library
                , containers       >= 0.4 && < 0.8
                , mtl              >= 2.0 && < 2.4
                , parsec           >= 2.0 && < 3.2
-               , copilot-language >= 4.3 && < 4.4
+               , copilot-language >= 4.4 && < 4.5
 
   exposed-modules:
       Copilot.Library.Libraries
diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG
index caec436ef..360d2e9a0 100644
--- a/copilot-prettyprinter/CHANGELOG
+++ b/copilot-prettyprinter/CHANGELOG
@@ -1,3 +1,6 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+
 2025-03-07
         * Version bump (4.3). (#604)
         * Update pretty-printing to handle Props. (#254)
diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
index 46e8de208..2a4a9578f 100644
--- a/copilot-prettyprinter/copilot-prettyprinter.cabal
+++ b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-prettyprinter
-version:             4.3
+version:             4.4
 synopsis:            A prettyprinter of Copilot Specifications.
 description:
   A prettyprinter of Copilot specifications.
@@ -45,7 +45,7 @@ library
     base   >= 4.9 && < 5,
     pretty >= 1.0 && < 1.2,
 
-    copilot-core >= 4.3 && < 4.4
+    copilot-core >= 4.4 && < 4.5
 
   exposed-modules:
 
diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
index d3c2bd464..f221aec44 100644
--- a/copilot-theorem/CHANGELOG
+++ b/copilot-theorem/CHANGELOG
@@ -1,3 +1,7 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+        * Translate quantifiers correctly in Kind2 backend. (#594)
+
 2025-03-07
         * Version bump (4.3). (#604)
         * Fix multiple typos in README. (#560)
diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
index c6994913f..ad7ab8699 100644
--- a/copilot-theorem/copilot-theorem.cabal
+++ b/copilot-theorem/copilot-theorem.cabal
@@ -14,7 +14,7 @@ description:
   <https://copilot-language.github.io>.
 
 
-version                   : 4.3
+version                   : 4.4
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -63,8 +63,8 @@ library
                           , xml                   >= 1.3 && < 1.4
                           , what4                 >= 1.3 && < 1.7
 
-                          , copilot-core          >= 4.3 && < 4.4
-                          , copilot-prettyprinter >= 4.3 && < 4.4
+                          , copilot-core          >= 4.4 && < 4.5
+                          , copilot-prettyprinter >= 4.4 && < 4.5
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
index 42a2f60dc..f80b8170b 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
@@ -8,19 +8,38 @@ import Text.XML.Light       hiding (findChild)
 import Copilot.Theorem.Prove  as P
 import Data.Maybe           (fromJust)
 
+import qualified Copilot.Core as C
+
 import qualified Copilot.Theorem.Misc.Error as Err
 
 simpleName s = QName s Nothing Nothing
 
 -- | Parse output of Kind2.
 parseOutput :: String    -- ^ Property whose validity is being checked.
+            -> C.Prop    -- ^ The property's quantifier.
             -> String    -- ^ XML output of Kind2
             -> P.Output
-parseOutput prop xml = fromJust $ do
+parseOutput propId propQuantifier xml = fromJust $ do
   root <- parseXMLDoc xml
   case findAnswer . findPropTag $ root of
-    "valid"       -> return (Output Valid   [])
-    "falsifiable" -> return (Output Invalid [])
+    "valid"       -> case propQuantifier of
+                       -- We encode a universally quantified property P as
+                       -- ∀x.P(x) in Kind2, so the original property is valid
+                       -- iff the Kind2 property is valid.
+                       C.Forall {} -> return (Output Valid   [])
+                       -- We encode an existentially quantified property P as
+                       -- ¬(∀x.¬(P(x))) in Kind2, so the original property is
+                       -- invalid iff the Kind2 property is valid.
+                       C.Exists {} -> return (Output Invalid [])
+    "falsifiable" -> case propQuantifier of
+                       -- We encode a universally quantified property P as
+                       -- ∀x.P(x) in Kind2, so the original property is invalid
+                       -- iff the Kind2 property is invalid.
+                       C.Forall {} -> return (Output Invalid [])
+                       -- We encode an existentially quantified property P as
+                       -- ¬(∀x.¬(P(x))) in Kind2, so the original property is
+                       -- valid iff the Kind2 property is invalid.
+                       C.Exists {} -> return (Output Valid   [])
     s             -> err $ "Unrecognized status : " ++ s
 
   where
@@ -31,10 +50,10 @@ parseOutput prop xml = fromJust $ do
       let rightElement elt =
             qName (elName elt) == "Property"
             && lookupAttr (simpleName "name") (elAttribs elt)
-                == Just prop
+                == Just propId
       in case filterChildren rightElement root of
            tag : _ -> tag
-           _ -> err $ "Tag for property " ++ prop ++ " not found"
+           _ -> err $ "Tag for property " ++ propId ++ " not found"
 
     findAnswer tag =
       case findChildren (simpleName "Answer") tag of
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
index 3931c615b..66db2c346 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
@@ -19,10 +19,12 @@ import Copilot.Theorem.Misc.Utils (openTempFile)
 
 import System.Process
 
-import System.Directory
-import Data.Default
+import           System.Directory
+import           Data.Default
+import qualified Data.Map         as Map
 
-import qualified Copilot.Theorem.TransSys as TS
+import qualified Copilot.Theorem.Misc.Error as Err
+import qualified Copilot.Theorem.TransSys   as TS
 
 -- | Options for Kind2
 data Options = Options
@@ -68,4 +70,12 @@ askKind2 (ProverST opts spec) assumptions toCheck = do
   putStrLn kind2Input
 
   removeFile tempName
-  return $ parseOutput (head toCheck) output
+
+  let propId         = head toCheck
+      propQuantifier = case Map.lookup propId (TS.specProps spec) of
+                         Just (_, quantifier) ->
+                           quantifier
+                         Nothing ->
+                           Err.impossible $
+                             "askKind2: " ++ propId ++ " not in specProps"
+  return $ parseOutput propId propQuantifier output
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
index d8115e893..123f6ed64 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs
@@ -65,7 +65,7 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props
     preds = map (trNode spec predCallsGraph) (specNodes spec)
     props = map trProp $
       filter ((`elem` checkedProps) . fst) $
-      Map.toList (specProps spec)
+        Map.toList $ Map.map fst $ specProps spec
 
 trProp :: (PropId, ExtVar) -> K.Prop
 trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var)
@@ -98,7 +98,7 @@ addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) =
 
     vars =
       let bindings   = nodeImportedVars (specTopNode spec)
-          toExtVar a = fromJust $ Map.lookup a (specProps spec)
+          toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec
           toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v
       in map (varName . toTopVar . toExtVar) assumptions
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
index 89fdc5787..3debe552c 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/PrettyPrint.hs
@@ -27,7 +27,8 @@ pSpec spec = items $$ props
     items = foldr (($$) . pNode) empty (specNodes spec)
     props = text "PROPS" $$
       Map.foldrWithKey (\k -> ($$) . pProp k)
-        empty (specProps spec)
+        empty
+        (Map.map fst (specProps spec))
 
 pProp pId extvar = quotes (text pId) <+> text "is" <+> pExtVar extvar
 
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
index d2a953387..b68181ae0 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
@@ -24,6 +24,8 @@ module Copilot.Theorem.TransSys.Spec
   , specDependenciesGraph
   , specTopNode ) where
 
+import qualified Copilot.Core as C
+
 import Copilot.Theorem.TransSys.Type
 import Copilot.Theorem.TransSys.Operators
 import Copilot.Theorem.TransSys.Invariants
@@ -51,11 +53,12 @@ type NodeId = String
 type PropId = String
 
 -- | A modular transition system is defined by a graph of nodes and a series
--- of properties, each mapped to a variable.
+-- of properties, each mapped to a variable and a 'C.Prop' describing how the
+-- property is quantified.
 data TransSys = TransSys
   { specNodes         :: [Node]
   , specTopNodeId     :: NodeId
-  , specProps         :: Map PropId ExtVar }
+  , specProps         :: Map PropId (ExtVar, C.Prop) }
 
 -- | A node is a set of variables living in a local namespace and corresponding
 -- to the 'Var' type.
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
index 79edd2828..e59058496 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
@@ -42,7 +42,8 @@ mergeNodes toMergeIds spec =
   spec
     { specNodes = newNode :
         map (updateOtherNode newNodeId toMergeIds renamingExtF) otherNodes
-    , specProps = Map.map renamingExtF (specProps spec) }
+    , specProps =
+        Map.map (\(ev, prop) -> (renamingExtF ev, prop)) (specProps spec) }
 
   where
     nodes = specNodes spec
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
index 68ddb8806..2659fa6cb 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
@@ -96,10 +96,12 @@ translate cspec =
     cprops :: [C.Property]
     cprops = C.specProperties cspec
 
-    propBindings :: Map PropId ExtVar
+    propBindings :: Map PropId (ExtVar, C.Prop)
     propBindings = Map.fromList $ do
-      pid <- map C.propertyName cprops
-      return (pid, mkExtVar topNodeId pid)
+      cprop <- cprops
+      let pid  = C.propertyName cprop
+          prop = C.propertyProp cprop
+      return (pid, (mkExtVar topNodeId pid, prop))
 
     ((modelNodes, propNodes), extvarNodesNames) = runTrans $
       liftM2 (,) (mapM stream (C.specStreams cspec)) (mkPropNodes cprops)
@@ -139,7 +141,15 @@ streamOfProp :: C.Property -> C.Stream
 streamOfProp prop =
   C.Stream { C.streamId = 42
            , C.streamBuffer = []
-           , C.streamExpr = C.extractProp (C.propertyProp prop)
+             -- TransSys encodes all properties using universal quantification.
+             -- Therefore, in order to encode an existentially quantified
+             -- property ∃x.P(x), we must first convert it to ¬(∀x.¬(P(x))).
+             -- The `Exists` case below handles the ∀x.¬(P(x)) part by adding
+             -- an `Op1 Not` around the property. The outermost negation is
+             -- handled elsewhere (e.g., in Copilot.Theorem.Kind2.Output.parse).
+           , C.streamExpr = case C.propertyProp prop of
+                              C.Forall p -> p
+                              C.Exists p -> C.Op1 C.Not p
            , C.streamExprType = C.Bool }
 
 stream :: C.Stream -> Trans Node
diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG
index abd146bba..b38dd2c3d 100644
--- a/copilot/CHANGELOG
+++ b/copilot/CHANGELOG
@@ -1,3 +1,7 @@
+2025-05-07
+        * Version bump (4.4). (#618)
+        * Update build status badge URL. (#612)
+
 2025-03-07
         * Version bump (4.3). (#604)
         * Include missing dependencies in installation instructions. (#591)
diff --git a/copilot/README.md b/copilot/README.md
index efdc58d28..893d6a933 100644
--- a/copilot/README.md
+++ b/copilot/README.md
@@ -2,7 +2,7 @@
 
 # Copilot
 
-[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot)
+[![Build Status](https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot)
 [![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](https://hackage.haskell.org/package/copilot)
 
 Copilot is a runtime verification framework for hard real-time systems.
diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal
index a39788ab8..6401ef883 100644
--- a/copilot/copilot.cabal
+++ b/copilot/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             4.3
+version:             4.4
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
@@ -52,12 +52,12 @@ library
                      , directory             >= 1.3  && < 1.4
                      , filepath              >= 1.4  && < 1.6
 
-                     , copilot-core          >= 4.3 && < 4.4
-                     , copilot-theorem       >= 4.3 && < 4.4
-                     , copilot-language      >= 4.3 && < 4.4
-                     , copilot-libraries     >= 4.3 && < 4.4
-                     , copilot-c99           >= 4.3 && < 4.4
-                     , copilot-prettyprinter >= 4.3 && < 4.4
+                     , copilot-core          >= 4.4 && < 4.5
+                     , copilot-theorem       >= 4.4 && < 4.5
+                     , copilot-language      >= 4.4 && < 4.5
+                     , copilot-libraries     >= 4.4 && < 4.5
+                     , copilot-c99           >= 4.4 && < 4.5
+                     , copilot-prettyprinter >= 4.4 && < 4.5
 
 
     exposed-modules: Language.Copilot, Language.Copilot.Main