diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 0543822f6..c98c74cf8 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -5,7 +5,7 @@ module Echidna.Campaign where
 
 import Control.Concurrent
 import Control.DeepSeq (force)
-import Control.Monad (replicateM, when, unless, void, forM_)
+import Control.Monad (replicateM, replicateM_, when, unless, void, forM_)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.Random.Strict (MonadRandom, RandT, evalRandT)
 import Control.Monad.Reader (MonadReader, asks, liftIO, ask)
@@ -20,10 +20,10 @@ import Data.List qualified as List
 import Data.List.NonEmpty qualified as NEList
 import Data.Map (Map, (\\))
 import Data.Map qualified as Map
-import Data.Maybe (isJust, mapMaybe, fromJust)
+import Data.Maybe (isJust, mapMaybe)
 import Data.Set (Set)
 import Data.Set qualified as Set
-import Data.Text (Text, unpack)
+import Data.Text (Text, pack, unpack)
 import Data.Time (LocalTime)
 import Data.Vector qualified as V
 import System.Random (mkStdGen)
@@ -40,9 +40,10 @@ import Echidna.Exec
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
 import Echidna.Solidity (chooseContract)
-import Echidna.SymExec.Common (extractTxs, extractErrors)
-import Echidna.SymExec.Exploration (exploreContract, getTargetMethodFromTx, getRandomTargetMethod)
+import Echidna.SymExec.Common (extractTxs, extractErrors, suitableForSymExec)
+import Echidna.SymExec.Exploration (exploreContract, exploreContractTwoPhase, exploreContractTwoPhaseProperty, getTargetMethodFromTx, getRandomTargetMethod)
 import Echidna.SymExec.Symbolic (forceAddr)
+import Echidna.SymExec.Property (verifyMethodForProperty, verifyMethodForAssertion, isSuitableForPropertyMode, isNoArgAssertionTarget)
 import Echidna.SymExec.Verification (verifyMethod, isSuitableToVerifyMethod)
 import Echidna.Test
 import Echidna.Transaction
@@ -52,9 +53,10 @@ import Echidna.Types.Corpus (Corpus, corpusSize)
 import Echidna.Types.Coverage (coverageStats)
 import Echidna.Types.Random (rElem)
 import Echidna.Types.Signature (FunctionName)
+import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Test
 import Echidna.Types.Test qualified as Test
-import Echidna.Types.Tx (TxCall(..), Tx(..))
+import Echidna.Types.Tx (TxCall(..), Tx(..), basicTx, maxGasPerBlock)
 import Echidna.Types.Worker
 import Echidna.Worker
 
@@ -116,7 +118,7 @@ runSymWorker
   -- ^ Initial corpus of transactions
   -> Maybe Text -- ^ Specified contract name
   -> m (WorkerStopReason, WorkerState)
-runSymWorker callback vm dict workerId _ name = do
+runSymWorker callback vm dict workerId initialCorpus name = do
   cfg <- asks (.cfg)
   let nworkers = getNFuzzWorkers cfg.campaignConf -- getNFuzzWorkers, NOT getNWorkers
   eventQueue <- asks (.eventQueue)
@@ -128,6 +130,15 @@ runSymWorker callback vm dict workerId _ name = do
         verifyMethods -- No arguments, everything is in this environment
         pure SymbolicVerificationDone
       else do
+        -- Run two-phase on initial corpus before listening for events
+        unless (null initialCorpus) $ do
+          pushWorkerEvent $ SymExecLog ("Two-phase on initial corpus (" <> show (length initialCorpus) <> " entries)")
+          forM_ initialCorpus $ \(_, txs) -> unless (null txs) $
+            replicateM_ cfg.campaignConf.symExecSeqSamples $ do
+              i <- rElem $ NEList.fromList [0 .. length txs]
+              let prefix = take i txs
+              vm' <- foldlM (\v tx -> snd <$> execTx v tx) vm prefix
+              symexecTx (Nothing, vm', prefix)
         lift callback
         listenerLoop listenerFunc chan nworkers
         pure SymbolicExplorationDone
@@ -199,7 +210,8 @@ runSymWorker callback vm dict workerId _ name = do
         pure Nothing
     shrinkLoop (n - 1)
 
-  symexecTxs onlyRandom txs = mapM_ symexecTx =<< txsToTxAndVmsSym onlyRandom txs
+  symexecTxs onlyRandom txs =
+    mapM_ symexecTx =<< txsToTxAndVmsSym onlyRandom txs
 
   -- | Turn a list of transactions into inputs for symexecTx:
   -- (list of txns we're on top of)
@@ -226,6 +238,13 @@ runSymWorker callback vm dict workerId _ name = do
     pure [(Nothing, rvm, rtxs)]
 
 
+  txsBaseLabel txs = case txs of
+    [] -> "initial state"
+    _  -> show (length txs) <> "-tx sequence ending with " <> showTxCall (last txs)
+    where showTxCall t = case t.call of
+            SolCall (n, _) -> unpack n
+            _ -> "unknown"
+
   symexecTx (tx, vm', txsBase) = do
     conf <- asks (.cfg)
     dapp <- asks (.dapp)
@@ -233,18 +252,39 @@ runSymWorker callback vm dict workerId _ name = do
     contract <- chooseContract cs name
     failedTests <- findFailedTests
     let failedTestSignatures = map getAssertionSignature failedTests
+    -- Single-phase exploration: only methods matching assertSigs filter
     case tx of
       Nothing -> getRandomTargetMethod contract conf.campaignConf.symExecTargets failedTestSignatures >>= \case
-        Nothing -> do
-          return ()
+        Nothing -> pure ()
         Just method -> exploreAndVerify contract method vm' txsBase
       Just t -> getTargetMethodFromTx t contract failedTestSignatures >>= \case
-        Nothing -> do
-          return ()
-        Just method -> do
-          exploreAndVerify contract method vm' txsBase
+        Nothing -> pure ()
+        Just method -> exploreAndVerify contract method vm' txsBase
+    -- Two-phase exploration for no-arg targets
+    testRefs <- asks (.testRefs)
+    tests <- liftIO $ traverse readIORef testRefs
+    let nSamples = conf.campaignConf.symExecSeqSamples
+        stateChanging = filter suitableForSymExec $ Map.elems contract.abiMap
+        noArgTargets
+          | isPropertyMode conf.solConf.testMode =
+              let propNames = [n | t <- tests, isOpen t, isPropertyTest t, PropertyTest n _ <- [t.testType]]
+              in filter (\m -> null m.inputs && m.name `elem` propNames) $ Map.elems contract.abiMap
+          | otherwise =
+              let assertSigs = [getAssertionSignature t | t <- tests, isOpen t, isAssertionTest t]
+              in filter (\m -> isNoArgAssertionTarget m && unpack m.methodSignature `elem` assertSigs) $ Map.elems contract.abiMap
+    unless (null noArgTargets || null stateChanging) $
+      replicateM_ nSamples $ do
+        method <- liftIO $ rElem (NEList.fromList stateChanging)
+        -- Sample ~20% of targets per iteration to avoid being too slow
+        let nTargetSamples = max 1 (length noArgTargets `div` 5)
+        sampledTargets <- List.nub <$> replicateM nTargetSamples (liftIO $ rElem (NEList.fromList noArgTargets))
+        let baseLabel = txsBaseLabel txsBase
+        if isPropertyMode conf.solConf.testMode
+          then exploreAndVerifyTwoPhaseProperty contract method sampledTargets vm' txsBase baseLabel
+          else exploreAndVerifyTwoPhase contract method sampledTargets vm' txsBase baseLabel
 
   exploreAndVerify contract method vm' txsBase = do
+    -- Single-phase exploration (existing)
     (threadId, symTxsChan) <- exploreContract contract method vm'
     modify' (\ws -> ws { runningThreads = [threadId] })
     lift callback
@@ -267,18 +307,241 @@ runSymWorker callback vm dict workerId _ name = do
       pushWorkerEvent $ SymExecError "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.")
     unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.")
 
+  exploreAndVerifyTwoPhase contract method targets vm' txsBase baseLabel = do
+    conf <- asks (.cfg)
+    let dst = conf.solConf.contractAddr
+    (threadId2, symTxsChan2) <- exploreContractTwoPhase contract method targets vm' baseLabel
+    modify' (\ws -> ws { runningThreads = [threadId2] })
+    lift callback
+
+    (symTxs2, partials2) <- liftIO $ takeMVar symTxsChan2
+    let txs2 = extractTxs symTxs2
+    let errors2 = extractErrors symTxs2
+
+    modify' (\ws -> ws { runningThreads = [] })
+    lift callback
+
+    -- For each concrete tx, execute it then check assertion functions
+    forM_ txs2 $ \symTx -> do
+      (_, vmAfter) <- execTx vm' symTx
+      case vmAfter.result of
+        Just (VMSuccess _) ->
+          updateTests $ \test -> do
+            if isOpen test && isAssertionTest test then do
+              let fnName = pack (getAssertionFunctionName test)
+                  assertTx = basicTx fnName [] symTx.src dst maxGasPerBlock (0, 0)
+              (_, vmCheck) <- execTx vmAfter assertTx
+              (testValue, vmCheck') <- checkETest test vmCheck
+              case testValue of
+                BoolValue False -> do
+                  wid <- Just <$> gets (.workerId)
+                  let test' = test { Test.state = Large 0
+                                   , reproducer = txsBase <> [symTx, assertTx]
+                                   , vm = Just vmAfter
+                                   , result = getResultFromVM vmCheck'
+                                   , Test.workerId = wid
+                                   }
+                  pushWorkerEvent (TestFalsified test')
+                  pure $ Just test'
+                _ -> pure Nothing
+            else pure Nothing
+        _ -> pure ()
+
+    unless (null errors2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error during two-phase assertion exploration: " <> show e)) errors2
+    unless (null partials2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial path during two-phase assertion exploration: " <> unpack e)) partials2
+
+  -- | Two-phase exploration for property mode: execute a state-changing method
+  -- symbolically, then check property functions against the resulting states.
+  exploreAndVerifyTwoPhaseProperty contract method targets vm' txsBase baseLabel = do
+    (threadId2, symTxsChan2) <- exploreContractTwoPhaseProperty contract method targets vm' baseLabel
+    modify' (\ws -> ws { runningThreads = [threadId2] })
+    lift callback
+
+    (symTxs2, partials2) <- liftIO $ takeMVar symTxsChan2
+    let txs2 = extractTxs symTxs2
+    let errors2 = extractErrors symTxs2
+
+    modify' (\ws -> ws { runningThreads = [] })
+    lift callback
+
+    -- For each concrete tx, execute it and check property functions
+    forM_ txs2 $ \symTx -> do
+      (_, vmAfter) <- execTx vm symTx
+      case vmAfter.result of
+        Just (VMSuccess _) ->
+          updateTests $ \test -> do
+            if isOpen test && isPropertyTest test then do
+              (testValue, vmCheck) <- checkETest test vmAfter
+              case testValue of
+                BoolValue False -> do
+                  wid <- Just <$> gets (.workerId)
+                  let test' = test { Test.state = Large 0
+                                   , reproducer = txsBase <> [symTx]
+                                   , vm = Just vmAfter
+                                   , result = getResultFromVM vmCheck
+                                   , Test.workerId = wid
+                                   }
+                  pushWorkerEvent (TestFalsified test')
+                  pure $ Just test'
+                _ -> pure Nothing
+            else pure Nothing
+        _ -> pure ()
+
+    unless (null errors2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error during two-phase property exploration: " <> show e)) errors2
+    unless (null partials2) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial path during two-phase property exploration: " <> unpack e)) partials2
+
   verifyMethods = do
     dapp <- asks (.dapp)
     let cs = Map.elems dapp.solcByName
     contract <- chooseContract cs name
     let allMethods = contract.abiMap
     conf <- asks (.cfg)
-    forM_ allMethods (\method -> do
-           isSuitable <- isSuitableToVerifyMethod contract method conf.campaignConf.symExecTargets
-           if isSuitable
-            then symExecMethod contract method
-            else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature)
-          )
+    if isPropertyMode conf.solConf.testMode
+      then verifyMethodsProperty contract allMethods
+      else verifyMethodsAssertion contract allMethods
+
+  -- | Assertion mode verification: single-phase for methods with args,
+  -- two-phase for no-arg assertion functions that can only fail via state.
+  verifyMethodsAssertion contract allMethods = do
+    conf <- asks (.cfg)
+    let methods = Map.elems allMethods
+        -- No-arg assertion functions: need two-phase
+        noArgAssertions = filter isNoArgAssertionTarget methods
+        -- State-changing methods with args: used as phase 1 targets
+        stateChangingMethods = filter suitableForSymExec methods
+
+    -- Single-phase for methods with args
+    forM_ allMethods $ \method -> do
+      isSuitable <- isSuitableToVerifyMethod contract method conf.campaignConf.symExecTargets
+      if isSuitable
+        then symExecMethod contract method
+        else pushWorkerEvent $ SymExecError ("Skipped verification of method " <> unpack method.methodSignature)
+
+    -- Two-phase for no-arg assertion functions
+    unless (null noArgAssertions || null stateChangingMethods) $ do
+      let targetNames = unwords $ map (unpack . (.methodSignature)) noArgAssertions
+      pushWorkerEvent $ SymExecLog ("Two-phase assertion verification for [" <> targetNames <> "]")
+      forM_ stateChangingMethods $ \method ->
+        symExecMethodAssertion contract method noArgAssertions
+
+  -- | Two-phase assertion mode: execute a state-changing method symbolically,
+  -- then check no-arg assertion functions against the resulting states.
+  symExecMethodAssertion contract method assertionTargets = do
+    lift callback
+    (threadId, symTxsChan) <- verifyMethodForAssertion assertionTargets method contract vm
+
+    modify' (\ws -> ws { runningThreads = [threadId] })
+    lift callback
+
+    (symTxs, partials) <- liftIO $ takeMVar symTxsChan
+    let txs = extractTxs symTxs
+    let errors = extractErrors symTxs
+
+    modify' (\ws -> ws { runningThreads = [] })
+    lift callback
+
+    let methodSignature = unpack method.methodSignature
+
+    pushWorkerEvent $ SymExecLog ("Assertion two-phase " <> methodSignature <> ": " <> show (length txs) <> " tx(es)")
+
+    conf <- asks (.cfg)
+    let dst = conf.solConf.contractAddr
+
+    -- For each concrete tx, execute it then explicitly call each assertion function
+    forM_ txs $ \symTx -> do
+      (_, vm') <- execTx vm symTx
+      case vm'.result of
+        Just (VMSuccess _) -> do
+          -- Re-execute each assertion function on the post-tx state,
+          -- then use checkETest which already handles all assertion patterns
+          updateTests $ \test -> do
+            if isOpen test && isAssertionTest test then do
+              let fnName = pack (getAssertionFunctionName test)
+                  assertTx = basicTx fnName [] symTx.src dst maxGasPerBlock (0, 0)
+              (_, vm'') <- execTx vm' assertTx
+              (testValue, vm''') <- checkETest test vm''
+              case testValue of
+                BoolValue False -> do
+                  wid <- Just <$> gets (.workerId)
+                  let test' = test { Test.state = Large 0
+                                   , reproducer = [symTx, assertTx]
+                                   , vm = Just vm'
+                                   , result = getResultFromVM vm'''
+                                   , Test.workerId = wid
+                                   }
+                  pushWorkerEvent (TestFalsified test')
+                  pure $ Just test'
+                _ -> pure Nothing
+            else pure Nothing
+        _ -> pure ()
+
+    unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during assertion two-phase for method " <> methodSignature <> ": " <> show e)) errors
+    unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during assertion two-phase for method " <> methodSignature <> ": " <> unpack e)) partials
+
+  -- | Property mode verification: symbolically execute each state-changing
+  -- method to find concrete inputs, then check property functions against
+  -- the resulting VM states.
+  verifyMethodsProperty contract allMethods = do
+    conf <- asks (.cfg)
+    let prefix = conf.solConf.prefix
+        targets = conf.campaignConf.symExecTargets
+        methods = Map.elems allMethods
+        stateChangingMethods = filter (\m -> isSuitableForPropertyMode m prefix targets) methods
+
+    when (null stateChangingMethods) $
+      pushWorkerEvent $ SymExecError "No suitable state-changing methods found for property verification"
+
+    forM_ stateChangingMethods $ \method ->
+      symExecMethodProperty contract method
+
+    pushWorkerEvent $ SymExecLog "Property verification finished"
+
+  -- | Symbolically execute a method in property mode: find concrete inputs
+  -- for all reachable paths, then check each against all property tests.
+  symExecMethodProperty contract method = do
+    lift callback
+    (threadId, symTxsChan) <- verifyMethodForProperty method contract vm
+
+    modify' (\ws -> ws { runningThreads = [threadId] })
+    lift callback
+
+    (symTxs, partials) <- liftIO $ takeMVar symTxsChan
+    let txs = extractTxs symTxs
+    let errors = extractErrors symTxs
+
+    modify' (\ws -> ws { runningThreads = [] })
+    lift callback
+
+    let methodSignature = unpack method.methodSignature
+
+    pushWorkerEvent $ SymExecLog ("Property two-phase " <> methodSignature <> ": " <> show (length txs) <> " tx(es)")
+
+    -- For each concrete tx from symbolic execution, execute it and check properties
+    forM_ txs $ \symTx -> do
+      (_, vm') <- execTx vm symTx
+      case vm'.result of
+        Just (VMSuccess _) -> do
+          -- Check all open property tests against the post-transaction state
+          updateTests $ \test -> do
+            if isOpen test && isPropertyTest test then do
+              (testValue, vm'') <- checkETest test vm'
+              case testValue of
+                BoolValue False -> do
+                  wid <- Just <$> gets (.workerId)
+                  let test' = test { Test.state = Large 0
+                                   , reproducer = [symTx]
+                                   , vm = Just vm'
+                                   , result = getResultFromVM vm''
+                                   , Test.workerId = wid
+                                   }
+                  pushWorkerEvent (TestFalsified test')
+                  pure $ Just test'
+                _ -> pure Nothing
+            else pure Nothing
+        _ -> pure ()
+
+    unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error during property verification of " <> methodSignature <> ": " <> show e)) errors
+    unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial path during property verification of " <> methodSignature <> ": " <> unpack e)) partials
 
   symExecMethod contract method = do
     lift callback
@@ -314,7 +577,7 @@ runSymWorker callback vm dict workerId _ name = do
         else
           pure $ Just test
 
-    pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.")
+    pushWorkerEvent $ SymExecLog "Assertion verification finished"
 
 -- | Run a fuzzing campaign given an initial universe state, some tests, and an
 -- optional dictionary to generate calls with. Return the 'Campaign' state once
diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs
index fcb1978ca..5578ab36b 100644
--- a/lib/Echidna/Config.hs
+++ b/lib/Echidna/Config.hs
@@ -111,6 +111,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "symExecMaxIters"    ..!= defaultSymExecMaxIters
         <*> v ..:? "symExecAskSMTIters" ..!= defaultSymExecAskSMTIters
         <*> v ..:? "symExecMaxExplore"  ..!= defaultSymExecMaxExplore
+        <*> v ..:? "symExecSeqSamples"   ..!= defaultSymExecSeqSamples
         where
         smtSolver = v ..:? "symExecSMTSolver" >>= \case
           Just ("z3" :: String)  -> pure Z3
diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index cae5d8d17..758f2795f 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -16,7 +16,7 @@ import Data.Set qualified as Set
 import Data.Text qualified as T
 import Optics.Core ((.~), (%), (%~))
 
-import EVM (loadContract, resetState, symbolify)
+import EVM (initialContract, loadContract, resetState, symbolify)
 import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..))
 import EVM.Effects (TTY, ReadConfig)
 import EVM.Expr qualified
@@ -25,7 +25,7 @@ import EVM.Format (formatPartialDetailed)
 import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..))
 import EVM.Solvers (SolverGroup)
 import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
-import EVM.Types (Addr, VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
+import EVM.Types (Addr, Contract(..), VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
 import qualified EVM.Types (VM(..))
 
 import Echidna.Test (isFoundryMode)
@@ -83,7 +83,8 @@ extractErrors = mapMaybe (\case
   _ -> Nothing)
 
 suitableForSymExec :: Method -> Bool
-suitableForSymExec m = not $ null m.inputs
+suitableForSymExec m =
+  not (null m.inputs)
   && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs)
   && not (T.isInfixOf "_no_symexec" m.name)
 
@@ -166,8 +167,14 @@ getUnknownLogs = mapMaybe (\case
 
 exploreMethod :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
   Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
+exploreMethod = exploreMethodWith Nothing
 
-exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
+-- | Like 'exploreMethod' but accepts a custom postcondition. When 'Nothing',
+-- uses the default assertion-checking postcondition.
+exploreMethodWith :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
+  Maybe Postcondition -> Method -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
+
+exploreMethodWith customPost method _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
   calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
   let
     cd = fst calldataSym
@@ -190,7 +197,98 @@ exploreMethod method _contract _sources vm defaultSender conf veriOpts solvers r
   -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
   -- Doing so might mess up concolic execution.
   let foundry = isFoundryMode conf.solConf.testMode
-  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1] foundry) Nothing
+  let postcondition = case customPost of
+        Just p  -> p
+        Nothing -> checkAssertions [0x1] foundry
+  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' postcondition Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
   --liftIO $ mapM_ print partials
   return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) partials)
+
+-- | Convert a symbolic contract expression (from a Success leaf) to a
+-- concrete Contract value suitable for use in a VM's env.contracts map.
+fromEContract :: Expr EContract -> Contract
+fromEContract (C code storage tStorage balance nonce) =
+  initialContract code
+    & #storage .~ storage
+    & #tStorage .~ tStorage
+    & #balance .~ balance
+    & #nonce .~ nonce
+fromEContract _ = error "fromEContract: unexpected non-C expression"
+
+-- | Two-phase symbolic execution.
+--
+-- Phase 1: Symbolically execute a state-changing method with a trivially-true
+-- postcondition (no solver calls). This collects all reachable Success leaves,
+-- each containing symbolic contract states and path constraints.
+--
+-- Phase 2: For each Success leaf and each target method, reconstruct a VM
+-- with the symbolic contract states, execute the target, and check the given
+-- postcondition. The solver finds concrete values for phase 1's symbolic
+-- variables (calldata, caller, etc.) that cause a violation.
+exploreMethodTwoPhase :: (MonadUnliftIO m, ReadConfig m, TTY m) =>
+  Postcondition -> Expr EAddr -> (Method -> m ()) -> Method -> [Method] -> SolcContract -> SourceCache -> EVM.Types.VM Concrete -> Addr -> EConfig -> VeriOpts -> SolverGroup -> Fetch.RpcInfo -> Fetch.Session -> m ([TxOrError], PartialsLogs)
+
+exploreMethodTwoPhase phase2Post phase2Caller logTarget method targetMethods _contract _sources vm defaultSender conf veriOpts solvers rpcInfo session = do
+  -- Phase 1: Execute state-changing method symbolically
+  calldataSym@(_, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+  let
+    cd = fst calldataSym
+    fetcher = Fetch.oracle solvers (Just session) rpcInfo
+    dst = conf.solConf.contractAddr
+  vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
+  let
+    vm' = vmReset & execState (loadContract (LitAddr dst))
+                  & #tx % #isCreate .~ False
+                  & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else TxValue)
+                  & #state % #caller .~ SymAddr "caller"
+                  & #state % #calldata .~ cd
+
+    vm'' = symbolify vm'
+        & #block %~ blockMakeSymbolic
+        & #constraints %~ (addBlockConstraints conf.txConf.maxTimeDelay conf.txConf.maxBlockDelay vm'.block)
+        & #constraints %~ (++ constraints ++ senderConstraints conf.solConf.sender)
+
+  -- Phase 1: PBool True postcondition → no solver calls, all Success paths return Qed
+  (phase1Models, phase1Partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (\_ _ -> PBool True) Nothing
+
+  -- Extract Success leaves with their path constraints and symbolic contract states
+  let successLeaves = [(props, contracts) | (_, Success props _ _ contracts) <- phase1Models]
+
+  -- Phase 2: For each Success leaf, check each target method
+  allResults <- concat <$> mapM (checkLeaf fetcher dst vm cd) successLeaves
+
+  let allPartialLogs = map (\(p, _) -> formatPartialDetailed Nothing Map.empty p) phase1Partials
+  return (allResults, allPartialLogs)
+
+  where
+
+  -- | Phase 2 for a single Success leaf: check all target methods
+  checkLeaf fetcher dst vm0 cd (leafConstraints, leafContracts) = do
+    let convertedContracts = Map.map fromEContract leafContracts
+    concat <$> mapM (checkTarget fetcher dst vm0 cd convertedContracts leafConstraints) targetMethods
+
+  -- | Phase 2 for a single (leaf, target) pair
+  checkTarget fetcher dst vm0 cd convertedContracts leafConstraints targetMethod = do
+    logTarget targetMethod
+    vmReset2 <- liftIO $ snd <$> runStateT (fromEVM resetState) vm0
+    let
+      targetCd = ConcreteBuf (selector targetMethod.methodSignature)
+      -- Replace contracts with phase 1's symbolic state, keeping originals as fallback
+      vm2 = vmReset2 & #env % #contracts %~ Map.union convertedContracts
+                     & execState (loadContract (LitAddr dst))
+                     & #tx % #isCreate .~ False
+                     & #state % #callvalue .~ Lit 0
+                     & #state % #caller .~ phase2Caller
+                     & #state % #calldata .~ targetCd
+      -- Carry over phase 1's path constraints so the solver must satisfy both phases
+      -- Reset exploration state so phase 2 gets fresh budget
+      vm2' = symbolify vm2
+          & #constraints .~ leafConstraints
+          & #iterations .~ mempty
+          & #pathsVisited .~ mempty
+          & #exploreDepth .~ 0
+
+    (phase2Models, _) <- verifyInputsWithHandler solvers veriOpts fetcher vm2' phase2Post Nothing
+    let results2 = filter (\(r, _) -> not (isQed r)) phase2Models & map fst
+    return $ map (modelToTx dst vm0.block.timestamp vm0.block.number method conf.solConf.sender defaultSender cd) results2
diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs
index fd4b2907b..191741340 100644
--- a/lib/Echidna/SymExec/Exploration.hs
+++ b/lib/Echidna/SymExec/Exploration.hs
@@ -8,7 +8,7 @@ import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO)
-import Control.Monad.State.Strict (MonadState)
+import Control.Monad.State.Strict (MonadState, gets)
 import Data.List.NonEmpty (fromList)
 import Data.Map qualified as Map
 import Data.Maybe (fromJust)
@@ -20,19 +20,22 @@ import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
 import EVM.Fetch (RpcInfo(..))
 import EVM.Solidity (SolcContract(..), Method(..))
 import EVM.Solvers (defMemLimit, withSolvers)
-import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..))
-import EVM.Types (VMType(..))
+import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..), Postcondition)
+import EVM.Types (VMType(..), EType(..), Expr(..))
 import qualified EVM.Types (VM(..))
 
-import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, rpcFetcher, TxOrError(..), PartialsLogs)
-import Echidna.Types.Campaign (CampaignConf(..), WorkerState)
+import Echidna.SymExec.Common (suitableForSymExec, exploreMethod, exploreMethodTwoPhase, checkAssertions, rpcFetcher, TxOrError(..), PartialsLogs)
+import Echidna.SymExec.Property (checkPropertyReturn)
+import Echidna.Test (isFoundryMode)
+import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..))
 import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..))
+import Echidna.Types.Test (TestConf(..))
 import Echidna.Types.Random (rElem)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..))
-import Echidna.Types.Worker (WorkerEvent(..))
+import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..))
 import Echidna.Types.World (World(..))
-import Echidna.Worker (pushWorkerEvent)
+import Echidna.Worker (pushWorkerEvent, pushCampaignEvent)
 
 -- | Uses symbolic execution to find transactions which would increase coverage.
 -- Spawns a new thread; returns its thread ID as the first return value.
@@ -102,7 +105,7 @@ exploreContract contract method vm = do
   let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
   let runtimeEnv = defaultEnv { config = hevmConfig }
   session <- asks (.fetchSession)
-  pushWorkerEvent $ SymExecLog ("Exploring " <> (show method.name))
+  pushWorkerEvent $ SymExecLog ("Exploring " <> unpack method.methodSignature)
   liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
     threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
       -- For now, we will be exploring a single method at a time.
@@ -116,3 +119,58 @@ exploreContract contract method vm = do
 
   threadId <- liftIO $ takeMVar threadIdChan
   pure (threadId, resultChan)
+
+-- | Two-phase exploration for assertion mode (symbolic caller).
+exploreContractTwoPhase :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContractTwoPhase contract method targetMethods vm baseLabel = do
+  conf <- asks (.cfg)
+  let isFoundry = isFoundryMode conf.solConf.testMode
+  exploreContractTwoPhaseWith (checkAssertions [0x1] isFoundry) (SymAddr "caller") contract method targetMethods vm baseLabel
+
+-- | Two-phase exploration for property mode (concrete test sender).
+exploreContractTwoPhaseProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContractTwoPhaseProperty contract method targetMethods vm baseLabel = do
+  conf <- asks (.cfg)
+  let dst = conf.solConf.contractAddr
+      propertySender = LitAddr (conf.testConf.testSender dst)
+  exploreContractTwoPhaseWith checkPropertyReturn propertySender contract method targetMethods vm baseLabel
+
+-- | Two-phase exploration parameterized by postcondition and phase 2 caller.
+exploreContractTwoPhaseWith :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => Postcondition -> Expr EAddr -> SolcContract -> Method -> [Method] -> EVM.Types.VM Concrete -> String -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+exploreContractTwoPhaseWith postcondition phase2Caller contract method targetMethods vm baseLabel = do
+  env <- ask
+  wid <- gets (.workerId)
+  let conf = env.cfg
+  dappInfo <- asks (.dapp)
+  let
+    timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = Just conf.campaignConf.symExecMaxIters
+    maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore)
+    askSmtIters = conf.campaignConf.symExecAskSMTIters
+    rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock))
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- liftIO newEmptyMVar
+  doneChan <- liftIO newEmptyMVar
+  resultChan <- liftIO newEmptyMVar
+  let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
+  let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased }
+  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive, dumpQueries = False }
+  let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo }
+  let runtimeEnv = defaultEnv { config = hevmConfig }
+  session <- asks (.fetchSession)
+  let methodSig = unpack method.methodSignature
+      logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Two-phase " <> baseLabel <> ": " <> methodSig <> " -> " <> unpack target.methodSignature)))
+  liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
+    threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
+      res <- exploreMethodTwoPhase postcondition phase2Caller logTarget method targetMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session
+      liftIO $ putMVar resultChan res
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- liftIO $ takeMVar threadIdChan
+  pure (threadId, resultChan)
diff --git a/lib/Echidna/SymExec/Property.hs b/lib/Echidna/SymExec/Property.hs
new file mode 100644
index 000000000..78025b72b
--- /dev/null
+++ b/lib/Echidna/SymExec/Property.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE GADTs #-}
+
+module Echidna.SymExec.Property where
+
+import Control.Applicative ((<|>))
+import Control.Concurrent (ThreadId, forkIO)
+import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
+import Control.Monad.Catch (MonadThrow(..))
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Reader (MonadReader, ask, asks, runReaderT, liftIO)
+import Control.Monad.State.Strict (MonadState, gets)
+import Data.Map qualified as Map
+import Data.Maybe (fromJust)
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+
+import EVM.Dapp (DappInfo(..))
+import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
+import EVM.Fetch (RpcInfo(..))
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (defMemLimit, withSolvers)
+import EVM.SymExec (IterConfig(..), LoopHeuristic(..), VeriOpts(..), Postcondition)
+import EVM.Types (Expr(..), Prop(..), VMType(..))
+import qualified EVM.Types (VM(..))
+
+import Echidna.SymExec.Common
+  ( rpcFetcher, checkAssertions, suitableForSymExec
+  , exploreMethodTwoPhase
+  , TxOrError(..), PartialsLogs
+  )
+import Echidna.Test (isFoundryMode)
+import Echidna.Types.Campaign (CampaignConf(..), WorkerState(..))
+import Echidna.Types.Config (Env(..), EConfig(..), OperationMode(..), OutputFormat(..), UIConf(..))
+import Echidna.Types.Test (TestConf(..))
+import Echidna.Types.Solidity (SolConf(..))
+import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..))
+import Echidna.Worker (pushCampaignEvent)
+
+-- | Postcondition for property mode phase 2: check if property function
+-- returned false (i.e., return value is 0).
+checkPropertyReturn :: Postcondition
+checkPropertyReturn _ = \case
+  Success _ _ returnBuf _ ->
+    PNeg (PEq (ReadWord (Lit 0) returnBuf) (Lit 0))
+  _ -> PBool True
+
+-- | Check if a method is suitable as a phase 1 target in property mode.
+isSuitableForPropertyMode :: Method -> Text.Text -> [Text.Text] -> Bool
+isSuitableForPropertyMode method prefix symExecTargets =
+  if null symExecTargets
+  then not (Text.isPrefixOf prefix method.name) && suitableForSymExec method
+  else method.name `elem` symExecTargets
+
+-- | Check if a method is a no-argument assertion function suitable for
+-- two-phase verification.
+isNoArgAssertionTarget :: Method -> Bool
+isNoArgAssertionTarget m = null m.inputs
+  && not (Text.isInfixOf "_no_symexec" m.name)
+
+-- | Spawn a thread for two-phase property mode verification.
+verifyMethodForProperty :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+verifyMethodForProperty method contract vm = do
+  env <- ask
+  wid <- gets (.workerId)
+  let conf = env.cfg
+  dappInfo <- asks (.dapp)
+  let
+    propertyMethods = filter (\m -> Text.isPrefixOf conf.solConf.prefix m.name) $ Map.elems contract.abiMap
+    timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = Just conf.campaignConf.symExecMaxIters
+    maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore)
+    askSmtIters = conf.campaignConf.symExecAskSMTIters
+    rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock))
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- liftIO newEmptyMVar
+  doneChan <- liftIO newEmptyMVar
+  resultChan <- liftIO newEmptyMVar
+  let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
+  let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased }
+  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive }
+  let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo }
+  let runtimeEnv = defaultEnv { config = hevmConfig }
+  session <- asks (.fetchSession)
+  let methodSig = Text.unpack method.methodSignature
+      logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Verifying property: " <> methodSig <> " -> " <> Text.unpack target.methodSignature)))
+
+  liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
+    let dst = conf.solConf.contractAddr
+        propertySender = LitAddr (conf.testConf.testSender dst)
+    threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
+      (res, partials) <- exploreMethodTwoPhase checkPropertyReturn propertySender logTarget method propertyMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session
+      liftIO $ putMVar resultChan (res, partials)
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- liftIO $ takeMVar threadIdChan
+  pure (threadId, resultChan)
+
+-- | Spawn a thread for two-phase assertion mode verification (no-arg functions).
+verifyMethodForAssertion :: (MonadIO m, MonadThrow m, MonadReader Echidna.Types.Config.Env m, MonadState WorkerState m)
+  => [Method] -> Method -> SolcContract -> EVM.Types.VM Concrete -> m (ThreadId, MVar ([TxOrError], PartialsLogs))
+verifyMethodForAssertion assertionMethods method contract vm = do
+  env <- ask
+  wid <- gets (.workerId)
+  let conf = env.cfg
+  dappInfo <- asks (.dapp)
+  let
+    isFoundry = isFoundryMode conf.solConf.testMode
+    timeoutSMT = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = Just conf.campaignConf.symExecMaxIters
+    maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore)
+    askSmtIters = conf.campaignConf.symExecAskSMTIters
+    rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock))
+    defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- liftIO newEmptyMVar
+  doneChan <- liftIO newEmptyMVar
+  resultChan <- liftIO newEmptyMVar
+  let isNonInteractive = conf.uiConf.operationMode == NonInteractive Text
+  let iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = StackBased }
+  let hevmConfig = defaultConfig { maxWidth = 5, maxDepth = maxExplore, dumpExprs = True, maxBufSize = 12, promiseNoReent = False, onlyDeployed = True, debug = isNonInteractive }
+  let veriOpts = VeriOpts { iterConf = iterConfig, rpcInfo = rpcInfo }
+  let runtimeEnv = defaultEnv { config = hevmConfig }
+  session <- asks (.fetchSession)
+  let methodSig' = Text.unpack method.methodSignature
+      logTarget target = liftIO $ pushCampaignEvent env (WorkerEvent wid SymbolicWorker (SymExecLog ("Verifying assertion: " <> methodSig' <> " -> " <> Text.unpack target.methodSignature)))
+
+  liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
+    threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
+      (res, partials) <- exploreMethodTwoPhase (checkAssertions [0x1] isFoundry) (SymAddr "caller") logTarget method assertionMethods contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session
+      liftIO $ putMVar resultChan (res, partials)
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- liftIO $ takeMVar threadIdChan
+  pure (threadId, resultChan)
diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs
index 7a3e80ed5..fc490369d 100644
--- a/lib/Echidna/SymExec/Verification.hs
+++ b/lib/Echidna/SymExec/Verification.hs
@@ -66,7 +66,7 @@ verifyMethod method contract vm = do
   let veriOpts = VeriOpts {iterConf = iterConfig, rpcInfo = rpcInfo}
   let runtimeEnv = defaultEnv { config = hevmConfig }
   session <- asks (.fetchSession)
-  pushWorkerEvent $ SymExecLog ("Verifying " <> (show method.name))
+  pushWorkerEvent $ SymExecLog ("Verifying " <> Text.unpack method.methodSignature)
 
   liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) timeoutSMT defMemLimit $ \solvers -> do
     threadId <- liftIO $ forkIO $ flip runReaderT runtimeEnv $ do
diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs
index 77dce6564..372eca198 100644
--- a/lib/Echidna/Types/Campaign.hs
+++ b/lib/Echidna/Types/Campaign.hs
@@ -67,6 +67,9 @@ data CampaignConf = CampaignConf
   , symExecMaxExplore :: Integer
     -- ^ Maximum number of states to explore before we stop exploring it.
     -- Only relevant if symExec is True
+  , symExecSeqSamples :: Int
+    -- ^ Number of random (method, split) samples for two-phase exploration
+    -- per coverage event. Only relevant if symExec is True
   }
 
 -- | The state of a fuzzing campaign.
@@ -117,6 +120,9 @@ defaultSymExecNWorkers = 1
 defaultSymExecMaxExplore :: Integer
 defaultSymExecMaxExplore = 10
 
+defaultSymExecSeqSamples :: Int
+defaultSymExecSeqSamples = 3
+
 defaultSymExecMaxIters :: Integer
 defaultSymExecMaxIters = 5
 
diff --git a/lib/Echidna/Types/Test.hs b/lib/Echidna/Types/Test.hs
index 1e998a8c9..4b189210a 100644
--- a/lib/Echidna/Types/Test.hs
+++ b/lib/Echidna/Types/Test.hs
@@ -117,6 +117,18 @@ instance ToJSON EchidnaTest where
     , "result" .= result
     ]
 
+isPropertyTest :: EchidnaTest -> Bool
+isPropertyTest EchidnaTest{testType = PropertyTest _ _} = True
+isPropertyTest _ = False
+
+getPropertyName :: EchidnaTest -> Text
+getPropertyName EchidnaTest{testType = PropertyTest n _} = n
+getPropertyName _ = error "Not a property test"
+
+getPropertyAddr :: EchidnaTest -> Addr
+getPropertyAddr EchidnaTest{testType = PropertyTest _ a} = a
+getPropertyAddr _ = error "Not a property test"
+
 isOptimizationTest :: EchidnaTest -> Bool
 isOptimizationTest EchidnaTest{testType = OptimizationTest _ _} = True
 isOptimizationTest _ = False
diff --git a/src/test/Common.hs b/src/test/Common.hs
index fc8ef8e79..6005348c8 100644
--- a/src/test/Common.hs
+++ b/src/test/Common.hs
@@ -1,10 +1,12 @@
 module Common
   ( testConfig
   , runContract
+  , runContractMultiWorker
   , testContract
   , testContractV
   , solcV
   , testContract'
+  , testContractMultiWorker
   , testContractNamed
   , checkConstructorConditions
   , optimized
@@ -23,6 +25,8 @@ module Common
   , gasConsumedGt
   ) where
 
+import Control.Concurrent (forkIO)
+import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar)
 import Control.Monad (forM_)
 import Control.Monad.Random (getRandomR)
 import Control.Monad.Reader (runReaderT)
@@ -44,6 +48,8 @@ import EVM.Types hiding (Env, Gas)
 
 import Echidna (mkEnv, prepareContract)
 import Echidna.Campaign (runWorker)
+import Echidna.Types.Worker (WorkerType(..), WorkerEvent(..), CampaignEvent(..))
+import Echidna.Worker (pushCampaignEvent)
 import Echidna.Config (parseConfig, defaultConfig)
 import Echidna.Solidity (selectMainContract, mkTests, loadSpecified, compileContracts)
 import Echidna.Test (checkETest)
@@ -53,7 +59,6 @@ import Echidna.Types.Signature (ContractName)
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Test
 import Echidna.Types.Tx (Tx(..), TxCall(..))
-import Echidna.Types.Worker (WorkerType(..))
 import Echidna.Types.World (World(..))
 
 testConfig :: EConfig
@@ -103,6 +108,49 @@ runContract f selectedContract cfg workerType = do
   -- be IO
   pure (env, finalState)
 
+-- | Run a contract with multiple workers (fuzz + symbolic) concurrently.
+-- Returns the env and the symbolic worker's state.
+runContractMultiWorker :: FilePath -> Maybe ContractName -> EConfig -> IO (Env, WorkerState)
+runContractMultiWorker f selectedContract cfg = do
+  seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
+  buildOutput <- compileContracts cfg.solConf (f :| [])
+  (vm, env, dict) <- prepareContract cfg (f :| []) buildOutput selectedContract seed
+  let nFuzz = getNFuzzWorkers cfg.campaignConf
+  -- Spawn fuzz workers, push WorkerStopped when done
+  forM_ [0..nFuzz-1] $ \wid ->
+    forkIO $ do
+      (stopReason, _) <- flip runReaderT env $
+        runWorker FuzzWorker (pure ()) vm dict wid [] cfg.campaignConf.testLimit selectedContract
+      pushCampaignEvent env (WorkerEvent wid FuzzWorker (WorkerStopped stopReason))
+  -- Spawn symbolic worker (last worker ID)
+  let symWid = nFuzz
+  symResult <- newEmptyMVar
+  _ <- forkIO $ do
+    result <- flip runReaderT env $
+      runWorker SymbolicWorker (pure ()) vm dict symWid [] cfg.campaignConf.testLimit selectedContract
+    putMVar symResult result
+  -- Wait for symbolic worker (it exits after all fuzz workers send WorkerStopped)
+  (_stopReason, finalState) <- takeMVar symResult
+  pure (env, finalState)
+
+testContractMultiWorker
+  :: FilePath
+  -> Maybe ContractName
+  -> Maybe SolcVersionComp
+  -> Maybe FilePath
+  -> [(String, (Env, WorkerState) -> IO Bool)]
+  -> TestTree
+testContractMultiWorker fp n v configPath expectations = testCase fp $ withSolcVersion v $ do
+  c <- case configPath of
+    Just path -> do
+      parsed <- parseConfig path
+      pure parsed.econfig
+    Nothing -> pure testConfig
+  let c' = c & overrideQuiet
+  result <- runContractMultiWorker fp n c'
+  forM_ expectations $ \(message, assertion) -> do
+    assertion result >>= assertBool message
+
 testContract
   :: FilePath
   -> Maybe FilePath
diff --git a/src/test/Tests/Symbolic.hs b/src/test/Tests/Symbolic.hs
index e3392078b..0a5eaaaea 100644
--- a/src/test/Tests/Symbolic.hs
+++ b/src/test/Tests/Symbolic.hs
@@ -2,7 +2,7 @@ module Tests.Symbolic (symbolicTests) where
 
 import Test.Tasty (TestTree, testGroup)
 
-import Common (testContract', solcV, solved, verified)
+import Common (testContract', testContractMultiWorker, solcV, solved, passed, verified)
 import Echidna.Types.Worker (WorkerType(..))
 
 symbolicTests :: TestTree
@@ -17,6 +17,24 @@ symbolicTests = testGroup "Symbolic tests" $
       , ("correct not verified", verified "correct")
       ]
   ) ["symbolic/verify.yaml", "symbolic/verify.bitwuzla.yaml"]
+  ++ [
+    testContract' "symbolic/verify-property.sol" (Just "PropertyVerifyTest") (Just (>= solcV (0,6,9))) (Just "symbolic/verify-property.yaml") True SymbolicWorker
+      [ ("echidna_x_is_not_ten falsified", solved "echidna_x_is_not_ten")
+      , ("echidna_x_is_not_one passed", passed "echidna_x_is_not_one")
+      , ("echidna_y_below_40 falsified", solved "echidna_y_below_40")
+      , ("echidna_locked_before_1000 falsified", solved "echidna_locked_before_1000")
+      ]
+  , testContract' "symbolic/verify-assertion-noarg.sol" (Just "AssertionNoArgTest") (Just (>= solcV (0,6,9))) (Just "symbolic/verify-assertion-noarg.yaml") True SymbolicWorker
+      [ ("check_x_not_ten falsified", solved "check_x_not_ten")
+      , ("check_y_below_100 falsified", solved "check_y_below_100")
+      , ("check_x_not_one passed", passed "check_x_not_one")
+      ]
+  ]
+  ++ [
+    testContractMultiWorker "symbolic/motiv.sol" (Just "Motiv") (Just (>= solcV (0,6,9))) (Just "symbolic/motiv-explore.yaml")
+      [ ("h() falsified", solved "h")
+      ]
+  ]
   ++ ([
     -- This test is commented out because it requires a specific setup where both the FuzzWorker and SymbolicWorker are used.
     -- If you run the symbolic worker alone, it will hang indefinitely.
diff --git a/tests/solidity/symbolic/motiv-explore.yaml b/tests/solidity/symbolic/motiv-explore.yaml
new file mode 100644
index 000000000..85a162625
--- /dev/null
+++ b/tests/solidity/symbolic/motiv-explore.yaml
@@ -0,0 +1,6 @@
+testMode: assertion
+symExec: true
+symExecSMTSolver: z3
+symExecSeqSamples: 10
+workers: 2
+testLimit: 100000
diff --git a/tests/solidity/symbolic/motiv.sol b/tests/solidity/symbolic/motiv.sol
new file mode 100644
index 000000000..a691a42fb
--- /dev/null
+++ b/tests/solidity/symbolic/motiv.sol
@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >=0.6.9;
+
+// Adapted from Smartian's motivating example.
+// Requires a 3-step chain: f(x) → g(y) → h()
+// where x % 32 == 1 and y == 72.
+contract Motiv {
+    address owner;
+    uint private stateA = 0;
+    uint private stateB = 0;
+    uint CONST = 32;
+
+    constructor() public {
+        owner = msg.sender;
+    }
+
+    function f(uint x) public {
+        if (msg.sender == owner) { stateA = x; }
+    }
+
+    function g(uint y) public {
+        if (stateA % CONST == 1) {
+            stateB = y - 10;
+        }
+    }
+
+    function h() public view {
+        assert(stateB != 62);
+    }
+}
diff --git a/tests/solidity/symbolic/motiv.yaml b/tests/solidity/symbolic/motiv.yaml
new file mode 100644
index 000000000..a5e2a935b
--- /dev/null
+++ b/tests/solidity/symbolic/motiv.yaml
@@ -0,0 +1,6 @@
+testMode: assertion
+symExec: true
+symExecSMTSolver: z3
+workers: 0
+seqLen: 1
+disableSlither: true
diff --git a/tests/solidity/symbolic/verify-assertion-noarg.sol b/tests/solidity/symbolic/verify-assertion-noarg.sol
new file mode 100644
index 000000000..330f24884
--- /dev/null
+++ b/tests/solidity/symbolic/verify-assertion-noarg.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >=0.6.9;
+
+// Test contract for two-phase assertion mode: no-arg assertion functions
+// that can only be falsified via state set by other functions.
+contract AssertionNoArgTest {
+    uint256 public x;
+    uint256 public y;
+
+    function set_x(uint256 _x) public {
+        require(_x >= 5, "too low");
+        require(_x <= 20, "too high");
+        x = _x;
+    }
+
+    function set_y(uint256 _y) public {
+        require(_y > 0, "must be positive");
+        y = _y;
+    }
+
+    // No-arg assertion: should be falsified when x == 10
+    function check_x_not_ten() public view {
+        assert(x != 10);
+    }
+
+    // No-arg assertion: should be falsified when y >= 100
+    function check_y_below_100() public view {
+        assert(y < 100);
+    }
+
+    // No-arg assertion: should never be falsified (x can't be 1 due to require >= 5)
+    function check_x_not_one() public view {
+        assert(x != 1);
+    }
+}
diff --git a/tests/solidity/symbolic/verify-assertion-noarg.yaml b/tests/solidity/symbolic/verify-assertion-noarg.yaml
new file mode 100644
index 000000000..a5e2a935b
--- /dev/null
+++ b/tests/solidity/symbolic/verify-assertion-noarg.yaml
@@ -0,0 +1,6 @@
+testMode: assertion
+symExec: true
+symExecSMTSolver: z3
+workers: 0
+seqLen: 1
+disableSlither: true
diff --git a/tests/solidity/symbolic/verify-property.sol b/tests/solidity/symbolic/verify-property.sol
new file mode 100644
index 000000000..41970b7fe
--- /dev/null
+++ b/tests/solidity/symbolic/verify-property.sol
@@ -0,0 +1,46 @@
+contract PropertyVerifyTest {
+  uint256 public x;
+  uint256 public y;
+  uint256 public lockedUntil;
+
+  function set_x(uint256 _x) public {
+    // Only values 5 <= _x <= 20 are accepted.
+    require(_x >= 5, "too low");
+    require(_x <= 20, "too high");
+    x = _x;
+  }
+
+  function set_y(uint256 _y) public {
+    // Only even values accepted
+    require(_y % 2 == 0, "must be even");
+    require(_y > 0, "must be positive");
+    y = _y;
+  }
+
+  function lock(uint256 duration) public {
+    require(duration > 0 && duration <= 365 days, "bad duration");
+    lockedUntil = block.timestamp + duration;
+  }
+
+  // Should be FALSIFIED: set_x(10) passes the requires and sets x == 10
+  function echidna_x_is_not_ten() public returns (bool) {
+    return x != 10;
+  }
+
+  // Should HOLD: set_x requires _x >= 5, so x can never be 1
+  function echidna_x_is_not_one() public returns (bool) {
+    return x != 1;
+  }
+
+  // Should be FALSIFIED: set_y(42) passes both requires
+  function echidna_y_below_40() public returns (bool) {
+    return y < 40;
+  }
+
+  // Should be FALSIFIED: lock() sets lockedUntil = block.timestamp + duration,
+  // and block.timestamp is symbolic, so the solver can pick a timestamp where
+  // lockedUntil > 1000.
+  function echidna_locked_before_1000() public returns (bool) {
+    return lockedUntil <= 1000;
+  }
+}
diff --git a/tests/solidity/symbolic/verify-property.yaml b/tests/solidity/symbolic/verify-property.yaml
new file mode 100644
index 000000000..2ef986085
--- /dev/null
+++ b/tests/solidity/symbolic/verify-property.yaml
@@ -0,0 +1,7 @@
+testMode: property
+symExec: true
+symExecSMTSolver: z3
+workers: 0
+seqLen: 1
+
+disableSlither: true