diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,12 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [0.4.1.0] -- 2024-01-10
+
+### Added
+
+- Added `cegisForAll` interfaces. ([#165])(https://github.com/lsrcz/grisette/pull/165)
+
 ## [0.4.0.0] -- 2024-01-08
 
 ### Added
@@ -125,6 +131,7 @@
 
 - Initial release for Grisette.
 
+[0.4.1.0]: https://github.com/lsrcz/grisette/compare/v0.4.1.0...v0.4.0.0
 [0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.3.1.0
 [0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1
 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -47,7 +47,7 @@
 ```cabal
 library
   ...
-  build-depends: grisette >= 0.4 < 0.5
+  build-depends: grisette >= 0.4.1 < 0.5
 ```
 
 #### Quick start template with `stack new`
diff --git a/grisette.cabal b/grisette.cabal
--- a/grisette.cabal
+++ b/grisette.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           grisette
-version:        0.4.0.0
+version:        0.4.1.0
 synopsis:       Symbolic evaluation as a library
 description:    Grisette is a reusable symbolic evaluation library for Haskell. By
                 translating programs into constraints, Grisette can help the development of
diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
--- a/src/Grisette/Core.hs
+++ b/src/Grisette/Core.hs
@@ -964,9 +964,9 @@
 
     -- ** CEGIS interfaces with pre/post conditions
     CEGISCondition (..),
-    cegisMultiInputs,
     cegisPostCond,
     cegisPrePost,
+    cegisMultiInputs,
     cegis,
     cegisExcept,
     cegisExceptStdVC,
@@ -974,6 +974,10 @@
     cegisExceptMultiInputs,
     cegisExceptStdVCMultiInputs,
     cegisExceptVCMultiInputs,
+    cegisForAll,
+    cegisForAllExcept,
+    cegisForAllExceptStdVC,
+    cegisForAllExceptVC,
 
     -- ** Symbolic constant extraction
 
@@ -1087,6 +1091,10 @@
     cegisExceptStdVCMultiInputs,
     cegisExceptVC,
     cegisExceptVCMultiInputs,
+    cegisForAll,
+    cegisForAllExcept,
+    cegisForAllExceptStdVC,
+    cegisForAllExceptVC,
     cegisMultiInputs,
     cegisPostCond,
     cegisPrePost,
diff --git a/src/Grisette/Core/Data/Class/CEGISSolver.hs b/src/Grisette/Core/Data/Class/CEGISSolver.hs
--- a/src/Grisette/Core/Data/Class/CEGISSolver.hs
+++ b/src/Grisette/Core/Data/Class/CEGISSolver.hs
@@ -33,9 +33,9 @@
 
     -- * CEGIS interfaces with pre/post conditions
     CEGISCondition (..),
-    cegisMultiInputs,
     cegisPostCond,
     cegisPrePost,
+    cegisMultiInputs,
     cegis,
     cegisExcept,
     cegisExceptStdVC,
@@ -43,6 +43,10 @@
     cegisExceptMultiInputs,
     cegisExceptStdVCMultiInputs,
     cegisExceptVCMultiInputs,
+    cegisForAll,
+    cegisForAllExcept,
+    cegisForAllExceptStdVC,
+    cegisForAllExceptVC,
   )
 where
 
@@ -275,7 +279,7 @@
 -- >>> :set -XOverloadedStrings
 -- >>> let [x,c] = ["x","c"] :: [SymInteger]
 -- >>> cegis (precise z3) x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))
--- ([...],CEGISSuccess (Model {c -> -1 :: Integer}))
+-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
 cegis ::
   ( ConfigurableSolver config handle,
     EvaluateSym inputs,
@@ -496,3 +500,115 @@
   (inputs -> t) ->
   IO ([inputs], CEGISResult SolvingFailure)
 cegisExceptStdVC config inputs = cegisExceptVC config inputs return
+
+-- |
+-- CEGIS with a single symbolic input to represent a set of inputs.
+--
+-- The following example tries to find the value of @c@ such that for all
+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make
+-- the solution unique.
+--
+-- >>> :set -XOverloadedStrings
+-- >>> let [x,c] = ["x","c"] :: [SymInteger]
+-- >>> cegisForAll (precise z3) x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)
+-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))
+cegisForAll ::
+  ( ExtractSymbolics forallInput,
+    ConfigurableSolver config handle
+  ) =>
+  config ->
+  -- | A symbolic value. All the symbolic constants in the value are treated as
+  -- for-all variables.
+  forallInput ->
+  CEGISCondition ->
+  -- | First output are the counter-examples for all the for-all variables, and
+  -- the second output is the model for all other variables if CEGIS succeeds.
+  IO ([Model], CEGISResult SolvingFailure)
+cegisForAll config input (CEGISCondition pre post) = do
+  (models, result) <- genericCEGIS config phi synthConstr () verifier
+  let exactResult = case result of
+        CEGISSuccess model -> CEGISSuccess $ exceptFor forallSymbols model
+        _ -> result
+  return (models, exactResult)
+  where
+    phi = pre .&& post
+    negphi = pre .&& symNot post
+    forallSymbols = extractSymbolics input
+    synthConstr _ model = return $ evaluateSym False model phi
+    verifier () candidate = do
+      let evaluated =
+            evaluateSym False (exceptFor forallSymbols candidate) negphi
+      r <- solve config evaluated
+      case r of
+        Left Unsat -> return ((), CEGISVerifierNoCex)
+        Left err -> return ((), CEGISVerifierException err)
+        Right model ->
+          return ((), CEGISVerifierFoundCex $ exact forallSymbols model)
+
+-- |
+-- CEGIS for symbolic programs with error handling, with a forall variable.
+--
+-- See 'cegisForAll' and 'cegisExcept'.
+cegisForAllExcept ::
+  ( UnionWithExcept t u e v,
+    UnionPrjOp u,
+    Functor u,
+    EvaluateSym inputs,
+    ExtractSymbolics inputs,
+    ConfigurableSolver config handle,
+    SEq inputs
+  ) =>
+  config ->
+  inputs ->
+  (Either e v -> CEGISCondition) ->
+  t ->
+  IO ([Model], CEGISResult SolvingFailure)
+cegisForAllExcept config inputs f v =
+  cegisForAll config inputs $ simpleMerge $ f <$> extractUnionExcept v
+
+-- |
+-- CEGIS for symbolic programs with error handling, with a forall variable.
+--
+-- See 'cegisForAll' and 'cegisExceptVC'.
+cegisForAllExceptVC ::
+  ( UnionWithExcept t u e v,
+    UnionPrjOp u,
+    Monad u,
+    EvaluateSym inputs,
+    ExtractSymbolics inputs,
+    ConfigurableSolver config handle,
+    SEq inputs
+  ) =>
+  config ->
+  inputs ->
+  (Either e v -> u (Either VerificationConditions ())) ->
+  t ->
+  IO ([Model], CEGISResult SolvingFailure)
+cegisForAllExceptVC config inputs f v = do
+  cegisForAll config inputs $
+    simpleMerge $
+      ( \case
+          Left AssumptionViolation -> cegisPrePost (con False) (con True)
+          Left AssertionViolation -> cegisPostCond (con False)
+          _ -> cegisPostCond (con True)
+      )
+        <$> (extractUnionExcept v >>= f)
+
+-- |
+-- CEGIS for symbolic programs with error handling, with a forall variable.
+--
+-- See 'cegisForAll' and 'cegisExceptStdVC'.
+cegisForAllExceptStdVC ::
+  ( UnionWithExcept t u VerificationConditions (),
+    UnionPrjOp u,
+    Monad u,
+    EvaluateSym inputs,
+    ExtractSymbolics inputs,
+    ConfigurableSolver config handle,
+    SEq inputs
+  ) =>
+  config ->
+  inputs ->
+  t ->
+  IO ([Model], CEGISResult SolvingFailure)
+cegisForAllExceptStdVC config inputs = cegisForAllExceptVC config inputs return
diff --git a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
@@ -7,7 +7,7 @@
 
 module Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) where
 
-import Control.Monad.Except (ExceptT, runExceptT)
+import Control.Monad.Except (ExceptT)
 import Data.Proxy (Proxy (Proxy))
 import qualified Data.SBV as SBV
 import Data.String (IsString (fromString))
@@ -24,6 +24,7 @@
   ( CEGISResult (CEGISSuccess),
     cegis,
     cegisExceptVC,
+    cegisForAllExceptVC,
     cegisMultiInputs,
     cegisPostCond,
   )
@@ -64,30 +65,35 @@
   (a -> [SymBool]) ->
   Assertion
 testCegis config shouldSuccess inputs bs = do
-  x <-
-    cegisExceptVC
-      config
-      (inputs, "internal" :: SymInteger)
-      return
-      ( \(cexInputs, internal) ->
-          runExceptT $ buildFormula internal (bs cexInputs)
-      )
-  case x of
+  cegisExceptVCResult <-
+    cegisExceptVC config (inputs, "internal" :: SymInteger) return $
+      \(cexInputs, internal) -> buildFormula internal (bs cexInputs)
+  case cegisExceptVCResult of
     (_, CEGISSuccess m) -> do
       shouldSuccess @=? True
-      verify (bs inputs)
-      where
-        verify [] = return ()
-        verify (v : vs) = do
-          y <- solve config (evaluateSym False m $ symNot v)
-          case y of
-            Left _ -> do
-              verify vs
-            Right _ ->
-              assertFailure $
-                "Failed to verify " ++ show v ++ " with the model " ++ show m
+      verify "cegisExceptVC" m (bs inputs)
     _ -> shouldSuccess @=? False
+  cegisForAllExceptVCResult <-
+    cegisForAllExceptVC config (inputs, "internal" :: SymInteger) return $
+      buildFormula "internal" (bs inputs)
+  case cegisForAllExceptVCResult of
+    (_, CEGISSuccess m) -> do
+      shouldSuccess @=? True
+      verify "cegisForAllExceptVC" m (bs inputs)
+    _ -> shouldSuccess @=? False
   where
+    verify _ _ [] = return ()
+    verify funName m (v : vs) = do
+      y <- solve config (evaluateSym False m $ symNot v)
+      case y of
+        Left _ -> verify funName m vs
+        Right _ ->
+          assertFailure $
+            funName
+              ++ ": Failed to verify "
+              ++ show v
+              ++ " with the model "
+              ++ show m
     buildFormula internal l = do
       symAssume (internal .>= 0)
       go l 0