diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2024-01-07
+        * Version bump (3.18). (#487)
+        * Introduce testing infrastructure for Copilot.Theorem.What4. (#474)
+        * Replace uses of forall with forAll. (#470)
+
 2023-11-07
         * Version bump (3.17). (#466)
         * Relax version constraint on what4. (#461)
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -14,7 +14,7 @@
   <https://copilot-language.github.io>.
 
 
-version                   : 3.17
+version                   : 3.18
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -63,8 +63,8 @@
                           , xml                   >= 1.3 && < 1.4
                           , what4                 >= 1.3 && < 1.6
 
-                          , copilot-core          >= 3.17 && < 3.18
-                          , copilot-prettyprinter >= 3.17 && < 3.18
+                          , copilot-core          >= 3.18 && < 3.19
+                          , copilot-prettyprinter >= 3.18 && < 3.19
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
@@ -108,3 +108,31 @@
                           , Copilot.Theorem.TransSys.Type
 
                           , Copilot.Theorem.What4.Translate
+
+test-suite unit-tests
+  type:
+    exitcode-stdio-1.0
+
+  main-is:
+    Main.hs
+
+  other-modules:
+    Test.Copilot.Theorem.What4
+
+  build-depends:
+      base
+    , QuickCheck
+    , test-framework
+    , test-framework-quickcheck2
+
+    , copilot-core
+    , copilot-theorem
+
+  hs-source-dirs:
+    tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,18 @@
+-- | Test copilot-theorem.
+module Main where
+
+-- External imports
+import Test.Framework (Test, defaultMain)
+
+-- Internal imports
+import qualified Test.Copilot.Theorem.What4
+
+-- | Run all unit tests on copilot-theorem.
+main :: IO ()
+main = defaultMain tests
+
+-- | All unit tests in copilot-theorem.
+tests :: [Test.Framework.Test]
+tests =
+  [ Test.Copilot.Theorem.What4.tests
+  ]
diff --git a/tests/Test/Copilot/Theorem/What4.hs b/tests/Test/Copilot/Theorem/What4.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Theorem/What4.hs
@@ -0,0 +1,108 @@
+-- The following warning is disabled due to a necessary instance of SatResult
+-- defined in this module.
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Test copilot-theorem:Copilot.Theorem.What4.
+module Test.Copilot.Theorem.What4 where
+
+-- External imports
+import Data.Int                             (Int8)
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Property, arbitrary, forAll)
+import Test.QuickCheck.Monadic              (monadicIO, run)
+
+-- External imports: Copilot
+import           Copilot.Core.Expr      (Expr (Const, Op2))
+import           Copilot.Core.Operators (Op2 (..))
+import           Copilot.Core.Spec      (Spec (..))
+import qualified Copilot.Core.Spec      as Copilot
+import           Copilot.Core.Type      (Typed (typeOf))
+
+-- Internal imports: Modules being tested
+import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)
+
+-- * Constants
+
+-- | Unit tests for copilot-theorem:Copilot.Theorem.What4.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Theorem.What4"
+    [ testProperty "Prove via Z3 that true is valid"    testProveZ3True
+    , testProperty "Prove via Z3 that false is invalid" testProveZ3False
+    , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst
+    ]
+
+-- * Individual tests
+
+-- | Test that Z3 is able to prove the following expression valid:
+-- @
+--   constant True
+-- @
+testProveZ3True :: Property
+testProveZ3True =
+    monadicIO $ run $ checkResult Z3 propName spec Valid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: Spec
+    spec = propSpec propName $ Const typeOf True
+
+-- | Test that Z3 is able to prove the following expression invalid:
+-- @
+--   constant False
+-- @
+testProveZ3False :: Property
+testProveZ3False =
+    monadicIO $ run $ checkResult Z3 propName spec Invalid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: Spec
+    spec = propSpec propName $ Const typeOf False
+
+-- | Test that Z3 is able to prove the following expresion valid:
+-- @
+--   for all (x :: Int8), constant x == constant x
+-- @
+testProveZ3EqConst :: Property
+testProveZ3EqConst = forAll arbitrary $ \x ->
+    monadicIO $ run $ checkResult Z3 propName (spec x) Valid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: Int8 -> Spec
+    spec x = propSpec propName $
+      Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
+
+-- | Check that the solver's satisfiability result for the given property in
+-- the given spec matches the expectation.
+checkResult :: Solver -> String -> Spec -> SatResult -> IO Bool
+checkResult solver propName spec expectation = do
+  results <- prove solver spec
+
+  -- Find the satisfiability result for propName.
+  let propResult = lookup propName results
+
+  -- The following check also works for the case in which the property name
+  -- does not exist in the results, in which case the lookup returns 'Nothing'.
+  return $ propResult == Just expectation
+
+-- * Auxiliary
+
+-- | Build a 'Spec' that contains one property with the given name and defined
+-- by the given boolean expression.
+propSpec :: String -> Expr Bool -> Spec
+propSpec propName propExpr = Spec [] [] [] [Copilot.Property propName propExpr]
+
+-- | Equality for 'SatResult'.
+--
+-- This is an orphan instance, so we suppress the warning that GHC would
+-- normally produce with a GHC option at the top.
+instance Eq SatResult where
+  Valid   == Valid   = True
+  Invalid == Invalid = True
+  Unknown == Unknown = True
+  _       == _       = False