diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index fd9f9a4f4..a97d7e8ba 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -232,11 +232,13 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v6
+        with:
+          submodules: recursive
 
       - name: Setup Python
         uses: actions/setup-python@v6
         with:
-          python-version: '3.8'
+          python-version: '3.10'
 
       - name: Install dependencies
         shell: bash
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 000000000..f7a1d4b99
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "tests/solidity/foundry/forge-std"]
+	path = tests/solidity/foundry/forge-std
+	url = https://github.com/foundry-rs/forge-std
diff --git a/README.md b/README.md
index d8dde7dd6..d1bbea583 100644
--- a/README.md
+++ b/README.md
@@ -54,6 +54,17 @@ $ echidna tests/solidity/basic/flags.sol
 
 Echidna should find a call sequence that falsifies `echidna_sometimesfalse` and should be unable to find a falsifying input for `echidna_alwaystrue`.
 
+### Testing modes
+
+The example above uses the default **property** mode, but Echidna supports several testing modes, configured via `testMode` in the config file or `--test-mode` on the CLI:
+
+* **`property`** (default): Test `echidna_`-prefixed functions that return `bool`.
+* **`assertion`**: Detect assertion failures from `assert()` and Foundry's `assertX` helpers (`assertTrue`, `assertEq`, etc.).
+* **`foundry`**: Run Foundry-style `test`-prefixed unit tests and `invariant_`-prefixed stateful invariants.
+* **`overflow`**: Detect integer over/underflows (Solidity >= 0.8.0).
+* **`optimization`**: Maximize the return value of `echidna_`-prefixed functions that return `int256` (uses the same configurable prefix as property mode).
+* **`exploration`**: Collect coverage without checking properties.
+
 ### Collecting and visualizing coverage
 
 After finishing a campaign, Echidna can save a coverage maximizing **corpus** in a special directory specified with the `corpusDir` config option. This directory will contain two entries: (1) a directory named `coverage` with JSON files that can be replayed by Echidna and (2) a plain-text file named `covered.txt`, a copy of the source code with coverage annotations.
@@ -143,8 +154,8 @@ Transaction = {
 
 `Coverage` is a dict describing certain coverage-increasing calls. These interfaces are
 subject to change to be slightly more user-friendly at a later date. `testType`
-will either be `property` or `assertion`, and `status` always takes on either
-`fuzzing`, `shrinking`, `solved`, `passed`, or `error`.
+will be one of `property`, `assertion`, `optimization`, `exploration`, or `call`,
+and `status` always takes on either `fuzzing`, `shrinking`, `solved`, `passed`, or `error`.
 
 ### Debugging Performance Problems
 
diff --git a/flake.nix b/flake.nix
index d82b516d6..ceed43464 100644
--- a/flake.nix
+++ b/flake.nix
@@ -62,8 +62,8 @@
           (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "argotorg";
             repo = "hevm";
-            rev = "41e6d1304411749ea8c816d131991663b5dca67a";
-            sha256 = "sha256-JF4IyQ3OvfrIqybtCvCpz6nw6kgo39LLJSxOjXsw3/c=";
+            rev = "ed90053fa0ed69e658a75ab0ed64d467f5a5448d";
+            sha256 = "sha256-drWR25sF1DyPie8oxXvI8N20Ee3YQ9l/7n9VIUg/wXY=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck
diff --git a/lib/Echidna.hs b/lib/Echidna.hs
index d77eac4e6..7e2ca900a 100644
--- a/lib/Echidna.hs
+++ b/lib/Echidna.hs
@@ -58,11 +58,12 @@ prepareContract
   -> IO (VM Concrete, Env, GenDict)
 prepareContract cfg solFiles buildOutput selectedContract seed = do
   let solConf = cfg.solConf
+      campaignConf = cfg.campaignConf
       (Contracts contractMap) = buildOutput.contracts
       contracts = Map.elems contractMap
 
   mainContract <- selectMainContract solConf selectedContract contracts
-  tests <- mkTests solConf mainContract
+  tests <- mkTests solConf campaignConf mainContract
   signatureMap <- mkSignatureMap solConf mainContract contracts
 
   -- run processors
diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs
index 28d55ee49..d99702bbc 100644
--- a/lib/Echidna/Exec.hs
+++ b/lib/Echidna/Exec.hs
@@ -56,6 +56,7 @@ classifyError = \case
   StackUnderrun        -> IllegalE
   BadJumpDestination   -> IllegalE
   IllegalOverflow      -> RevertE
+  AssumeCheatFailed    -> RevertE
   _                    -> UnknownE
 
 -- | Extracts the 'Query' if there is one.
diff --git a/lib/Echidna/Output/Foundry.hs b/lib/Echidna/Output/Foundry.hs
index 943744f32..4f294a4a9 100644
--- a/lib/Echidna/Output/Foundry.hs
+++ b/lib/Echidna/Output/Foundry.hs
@@ -76,7 +76,10 @@ foundryTx senders tx =
         prelude =
           (if time > 0 || blocks > 0 then "    _delay(" ++ show time ++ ", " ++ show blocks ++ ");\n" else "") ++
           "    _setUpActor(" ++ senderName ++ ");"
-        call = "    Target." ++ unpack name ++ "(" ++ foundryArgs (map abiValueToString args) ++ ");"
+        -- Handle fallback function (empty name).
+        call = if unpack name == ""
+          then "    address(Target).call(\"\");"
+          else "    Target." ++ unpack name ++ "(" ++ foundryArgs (map abiValueToString args) ++ ");"
       in Just $ object ["prelude" .= prelude, "call" .= call]
     _ -> Nothing
 
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index fd27b061c..2e585d401 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -41,7 +41,7 @@ import Echidna.ABI
 import Echidna.Deploy (deployContracts, deployBytecodes)
 import Echidna.Exec (execTx, execTxWithCov, initialVM)
 import Echidna.SourceAnalysis.Slither
-import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
+import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isFoundryMode)
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
@@ -146,11 +146,19 @@ filterMethods contractName (Whitelist ic) ms =
 filterMethods contractName (Blacklist ig) ms =
   NE.filter (\s -> encodeSigWithName contractName s `notElem` ig) ms
 
--- | Filter methods with arguments, used for dapptest mode
+-- | Filter methods for foundry mode. Per Foundry conventions:
+-- - Functions prefixed with "test" are test functions (unit or fuzz).
+--   Fuzz tests are distinguished by having at least one parameter.
+--   See: https://book.getfoundry.sh/forge/fuzz-testing
+-- - Functions prefixed with "invariant_" are invariant tests, called in
+--   randomized sequences to verify properties that must always hold.
+--   See: https://book.getfoundry.sh/forge/invariant-testing
+-- - Other functions with arguments are kept as callable targets for
+--   invariant test campaigns.
 filterMethodsWithArgs :: NonEmpty SolSignature -> NonEmpty SolSignature
 filterMethodsWithArgs ms =
-  case NE.filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ms of
-    [] -> error "No dapptest tests found"
+  case NE.filter (\(n, xs) -> T.isPrefixOf "test" n || (T.isPrefixOf "invariant_" n || not (null xs))) ms of
+    [] -> error "No foundry tests found"
     fs -> NE.fromList fs
 
 abiOf :: Text -> SolcContract -> NonEmpty SolSignature
@@ -223,16 +231,17 @@ loadSpecified env mainContract cs = do
                                            solConf.contractAddr
                                            unlimitedGasPerBlock
                                            (0, 0)
-    vm4 <- if isDapptestMode solConf.testMode && setUpFunction `elem` abi
+    vm4 <- if is_testFunction `elem` abi && setUpFunction `elem` abi
               then snd <$> transaction
               else pure vm3
 
     case vm4.result of
-      Just (VMFailure _) -> throwM SetUpCallFailed
+      Just (VMFailure _) -> throwM $ SetUpCallFailed $ showTraceTree env.dapp vm4
       _ -> pure vm4
 
   where
     setUpFunction = ("setUp", [])
+    is_testFunction = ("IS_TEST", [])
 
 
 selectMainContract
@@ -259,7 +268,7 @@ mkSignatureMap
 mkSignatureMap solConf mainContract contracts = do
   let
     -- Filter ABI according to the config options
-    fabiOfc = if isDapptestMode solConf.testMode
+    fabiOfc = if isFoundryMode solConf.testMode
                 then NE.toList $ filterMethodsWithArgs (abiOf solConf.prefix mainContract)
                 else filterMethods mainContract.contractName solConf.methodFilter $
                        abiOf solConf.prefix mainContract
@@ -276,7 +285,7 @@ mkSignatureMap solConf mainContract contracts = do
         case NE.nonEmpty fabiOfc of
           Just ne -> Map.singleton mainContract.runtimeCodehash ne
           Nothing -> mempty
-  when (null abiMapping && isDapptestMode solConf.testMode) $
+  when (null abiMapping && isFoundryMode solConf.testMode) $
     throwM NoTests
   when (Map.null abiMapping) $
     throwM $ InvalidMethodFilters solConf.methodFilter
@@ -284,14 +293,15 @@ mkSignatureMap solConf mainContract contracts = do
 
 mkTests
   :: SolConf
+  -> CampaignConf
   -> SolcContract
   -> IO [EchidnaTest]
-mkTests solConf mainContract = do
+mkTests solConf campaignConf mainContract = do
   let
     -- generate the complete abi mapping
     abi = Map.elems mainContract.abiMap <&> \method -> (method.name, snd <$> method.inputs)
     (tests, funs) = partition (isPrefixOf solConf.prefix . fst) abi
-    -- Filter again for dapptest tests or assertions checking if enabled
+    -- Filter again for foundry tests or assertions checking if enabled
     neFuns = filterMethods mainContract.contractName
                            solConf.methodFilter
                            (fallback NE.:| funs)
@@ -309,6 +319,7 @@ mkTests solConf mainContract = do
   pure $ createTests solConf.testMode
                      solConf.testDestruction
                      testNames
+                     campaignConf.seqLen
                      solConf.contractAddr
                      neFuns
 
@@ -348,7 +359,7 @@ mkWorld SolConf{sender, testMode} sigMap maybeContract slitherInfo contracts =
     payableSigs = filterResults maybeContract slitherInfo.payableFunctions
     assertSigs = filterResults maybeContract (assertFunctionList <$> slitherInfo.asserts)
     as = if isAssertionMode testMode then filterResults maybeContract (assertFunctionList <$> slitherInfo.asserts) else []
-    cs = if isDapptestMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
+    cs = if isFoundryMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
     (highSignatureMap, lowSignatureMap) = prepareHashMaps cs as $
       filterFallbacks slitherInfo.fallbackDefined slitherInfo.receiveDefined contracts sigMap
   in World { senders = sender
diff --git a/lib/Echidna/SourceAnalysis/Slither.hs b/lib/Echidna/SourceAnalysis/Slither.hs
index 11df9c579..5ccd5e7fb 100644
--- a/lib/Echidna/SourceAnalysis/Slither.hs
+++ b/lib/Echidna/SourceAnalysis/Slither.hs
@@ -3,6 +3,7 @@
 module Echidna.SourceAnalysis.Slither where
 
 import Control.Applicative ((<|>))
+import Control.Monad (unless)
 import Data.Aeson ((.:), (.:?), (.!=), eitherDecode, parseJSON, withEmbeddedJSON, withObject)
 import Data.Aeson.Types (FromJSON, Parser, Value(String))
 import Data.ByteString.Base16 qualified as BS16 (decode)
@@ -147,16 +148,18 @@ instance FromJSON SlitherInfo where
 runSlither :: FilePath -> SolConf -> IO SlitherInfo
 runSlither fp solConf = if solConf.disableSlither
   then do
-    hPutStrLn stderr $
-        "WARNING: Slither was explicitly disabled. Echidna uses Slither (https://github.com/crytic/slither)"
-        <> " to perform source analysis, which makes fuzzing more effective. You should enable it."
+    unless solConf.quiet $
+      hPutStrLn stderr
+        ( "WARNING: Slither was explicitly disabled. Echidna uses Slither (https://github.com/crytic/slither)"
+        <> " to perform source analysis, which makes fuzzing more effective. You should enable it." )
     pure emptySlitherInfo
   else findExecutable "slither" >>= \case
     Nothing -> do
-      hPutStrLn stderr $
-        "WARNING: slither not found. Echidna uses Slither (https://github.com/crytic/slither)"
-        <> " to perform source analysis, which makes fuzzing more effective. You should install it with"
-        <> " 'pip3 install slither-analyzer --user'"
+      unless solConf.quiet $
+        hPutStrLn stderr
+          ( "WARNING: slither not found. Echidna uses Slither (https://github.com/crytic/slither)"
+          <> " to perform source analysis, which makes fuzzing more effective. You should install it with"
+          <> " 'pip3 install slither-analyzer --user'" )
       pure emptySlitherInfo
     Just path -> do
       let args = ["--ignore-compile", "--print", "echidna", "--json", "-"]
diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index 5731e8801..cae5d8d17 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -1,7 +1,13 @@
+{-# LANGUAGE GADTs #-}
+
 module Echidna.SymExec.Common where
 
 import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO)
 import Control.Monad.State.Strict (execState, runStateT)
+import Data.ByteString (ByteString)
+import Data.ByteString qualified as BS
+import Data.DoubleWord (Word256)
+import Data.List (foldl')
 import Data.Function ((&))
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, mapMaybe)
@@ -11,22 +17,56 @@ import Data.Text qualified as T
 import Optics.Core ((.~), (%), (%~))
 
 import EVM (loadContract, resetState, symbolify)
-import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..))
+import EVM.ABI (abiKind, AbiKind(Dynamic), Sig(..), decodeBuf, AbiVals(..), selector, encodeAbiValue, AbiValue(..))
 import EVM.Effects (TTY, ReadConfig)
 import EVM.Expr qualified
 import EVM.Fetch qualified as Fetch
 import EVM.Format (formatPartialDetailed)
-import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData(..))
+import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..))
 import EVM.Solvers (SolverGroup)
-import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), checkAssertions, subModel, defaultSymbolicValues)
-import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
+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 qualified EVM.Types (VM(..))
 
+import Echidna.Test (isFoundryMode)
 import Echidna.Types (fromEVM)
 import Echidna.Types.Config (EConfig(..))
 import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..), maxGasPerBlock)
 
+panicMsg :: Word256 -> ByteString
+panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
+
+-- | Postcondition for symbolic execution verification.
+-- In foundry mode, all reverts are failures except vm.assume failures.
+-- In assertion mode, only assertion failures (0xfe opcode, Error(string)
+-- "assertion failed", or Panic codes) are detected.
+checkAssertions :: [Word256] -> Bool -> Postcondition
+checkAssertions errs isFoundry _ vmres
+  | isFoundry = case vmres of
+      -- vm.assume failures should not be treated as test failures
+      Failure _ _ AssumeCheatFailed -> PBool True
+      -- All other failures are test failures in foundry mode
+      Failure {} -> PBool False
+      _ -> PBool True
+  | otherwise = case vmres of
+      -- Solidity assert() opcode (0xfe)
+      Failure _ _ (UnrecognizedOpcode 0xfe) -> PBool False
+      -- Concrete revert: check for "assertion failed" message or panic code
+      Failure _ _ (Revert (ConcreteBuf msg)) ->
+        -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
+        let assertFail = selector "Error(string)" `BS.isPrefixOf` msg
+              && "assertion failed" `BS.isPrefixOf` BS.drop txtOffset msg
+        in PBool $ not (assertFail || msg `elem` fmap panicMsg errs)
+      -- Symbolic revert: check symbolically against panic messages
+      -- TODO: also check for Error(string) "assertion failed" in partially-symbolic
+      -- buffers, similar to hevm's symbolicFail in EVM.UnitTest
+      Failure _ _ (Revert b) ->
+        foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)
+      _ -> PBool True
+  where
+    txtOffset = 4 + 32 + 32 -- selector + offset + length
+
 type PartialsLogs = [T.Text]
 
 data TxOrError = TxFromResult Tx | SMTErrorFromResult String
@@ -127,7 +167,7 @@ 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 method contract sources vm defaultSender conf veriOpts solvers rpcInfo session = do
+exploreMethod 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
@@ -137,7 +177,8 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   let
     vm' = vmReset & execState (loadContract (LitAddr dst))
                   & #tx % #isCreate .~ False
-                  & #state % #callvalue .~ TxValue
+                  -- Foundry tests cannot accept ether, force callvalue to zero
+                  & #state % #callvalue .~ (if isFoundryMode conf.solConf.testMode then Lit 0 else TxValue)
                   & #state % #caller .~ SymAddr "caller"
                   & #state % #calldata .~ cd
 
@@ -148,8 +189,8 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
 
   -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
   -- Doing so might mess up concolic execution.
-  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1]) Nothing
+  let foundry = isFoundryMode conf.solConf.testMode
+  (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1] foundry) Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
-  let warnData = Just $ WarningData contract sources vm'
-  --liftIO $ mapM_ TIO.putStrLn partials
-  return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) partials)
+  --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)
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index fb13c636e..be277953d 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -52,13 +52,13 @@ createTest m = EchidnaTest Open m v [] Stop Nothing Nothing
 
 validateTestModeError :: String
 validateTestModeError =
-  "Invalid test mode (should be property, assertion, dapptest, optimization, overflow or exploration)"
+  "Invalid test mode (should be property, assertion, foundry, optimization, overflow or exploration)"
 
 validateTestMode :: String -> TestMode
 validateTestMode s = case s of
   "property"     -> s
   "assertion"    -> s
-  "dapptest"     -> s
+  "foundry"      -> s
   "exploration"  -> s
   "overflow"     -> s
   "optimization" -> s
@@ -76,18 +76,19 @@ isPropertyMode :: TestMode -> Bool
 isPropertyMode "property" = True
 isPropertyMode _          = False
 
-isDapptestMode :: TestMode -> Bool
-isDapptestMode "dapptest"  = True
-isDapptestMode _           = False
+isFoundryMode :: TestMode -> Bool
+isFoundryMode "foundry" = True
+isFoundryMode _          = False
 
 createTests
   :: TestMode
   -> Bool
   -> [Text]
+  -> Int
   -> Addr
   -> [SolSignature]
   -> [EchidnaTest]
-createTests m td ts r ss = case m of
+createTests m td ts seqLen r ss = case m of
   "exploration" ->
     [createTest Exploration]
   "overflow" ->
@@ -99,9 +100,15 @@ createTests m td ts r ss = case m of
   "assertion" ->
     map (\s -> createTest (AssertionTest False s r))
         (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)]
-  "dapptest" ->
-    map (\s -> createTest (AssertionTest True s r))
-        (filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ss)
+  -- In foundry mode, seqLen distinguishes fuzz tests (seqLen == 1) from
+  -- invariant tests (seqLen > 1), which determines how functions are filtered.
+  "foundry" ->
+    if seqLen == 1 then
+      map (\s -> createTest (AssertionTest True s r))
+        (filter (\(n, xs) -> T.isPrefixOf "test" n && not (null xs)) ss)
+    else
+      map (\s -> createTest (AssertionTest True s r))
+          (filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ss)
   _ -> error validateTestModeError
   ++ (if td then [sdt, sdat] else [])
   where
@@ -143,7 +150,7 @@ checkETest test vm = case test.testType of
   Exploration -> pure (BoolValue True, vm) -- These values are never used
   PropertyTest n a -> checkProperty vm n a
   OptimizationTest n a -> checkOptimization vm n a
-  AssertionTest dt n a -> if dt then checkDapptestAssertion vm n a
+  AssertionTest dt n a -> if dt then checkFoundryAssertion vm n a
                                 else checkStatefulAssertion vm n a
   CallTest _ f -> checkCall vm f
 
@@ -215,7 +222,9 @@ checkStatefulAssertion vm sig addr = do
     -- Whether the last transaction executed opcode 0xfe, meaning an assertion failure.
     isAssertionFailure = case vm.result of
       Just (VMFailure (UnrecognizedOpcode 0xfe)) -> True
+      Just (VMFailure (Revert (ConcreteBuf msg))) -> "assertion failed" `BS.isPrefixOf` BS.drop txtOffset msg
       _ -> False
+    txtOffset = 4+32+32 -- selector + offset + length
     -- Test always passes if it doesn't target the last executed contract and function.
     -- Otherwise it passes if it doesn't cause an assertion failure.
     events = extractEvents False dappInfo vm
@@ -223,16 +232,13 @@ checkStatefulAssertion vm sig addr = do
     isFailure = isCorrectTarget && (eventFailure || isAssertionFailure)
   pure (BoolValue (not isFailure), vm)
 
-assumeMagicReturnCode :: BS.ByteString
-assumeMagicReturnCode = "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0"
-
-checkDapptestAssertion
+checkFoundryAssertion
   :: (MonadReader Env m, MonadThrow m)
   => VM Concrete
   -> SolSignature
   -> Addr
   -> m (TestValue, VM Concrete)
-checkDapptestAssertion vm sig addr = do
+checkFoundryAssertion vm sig addr = do
   let
     -- Whether the last transaction has any value
     hasValue = vm.state.callvalue /= Lit 0
@@ -241,8 +247,10 @@ checkDapptestAssertion vm sig addr = do
       BS.isPrefixOf (BS.take 4 (abiCalldata (encodeSig sig) mempty))
                     (forceBuf vm.state.calldata)
     isAssertionFailure = case vm.result of
-      Just (VMFailure (Revert (ConcreteBuf bs))) ->
-        not $ BS.isSuffixOf assumeMagicReturnCode bs
+      -- vm.assume failures should not be treated as test failures
+      Just (VMFailure AssumeCheatFailed) -> False
+      Just (VMFailure (Revert _)) ->
+        T.isPrefixOf "test" (fst sig) || T.isPrefixOf "invariant_" (fst sig)
       Just (VMFailure _) -> True
       _ -> False
     isCorrectAddr = LitAddr addr == vm.state.codeContract
diff --git a/lib/Echidna/Types/Solidity.hs b/lib/Echidna/Types/Solidity.hs
index 01368ac5a..5b1115717 100644
--- a/lib/Echidna/Types/Solidity.hs
+++ b/lib/Echidna/Types/Solidity.hs
@@ -30,7 +30,7 @@ data SolException
   | OnlyTests
   | ConstructorArgs String
   | DeploymentFailed Addr Text
-  | SetUpCallFailed
+  | SetUpCallFailed Text
   | NoCryticCompile
   | InvalidMethodFilters Filter
   | OutdatedSolcVersion Version
@@ -50,7 +50,7 @@ instance Show SolException where
     ConstructorArgs s      -> "Constructor arguments are required: " ++ s
     NoCryticCompile        -> "crytic-compile not installed or not found in PATH. To install it, run:\n   pip install crytic-compile"
     InvalidMethodFilters f -> "Applying the filter " ++ show f ++ " to the methods produces an empty list. Are you filtering the correct functions using `filterFunctions` or fuzzing the correct contract?"
-    SetUpCallFailed        -> "Calling the setUp() function failed (revert, out-of-gas, sending ether to a non-payable constructor, etc.)"
+    SetUpCallFailed t      -> "Calling the setUp() function failed (revert, out-of-gas, sending ether to a non-payable constructor, etc.):\n" ++ unpack t
     DeploymentFailed a t   -> "Deploying the contract " ++ show a ++ " failed (revert, out-of-gas, sending ether to a non-payable constructor, etc.):\n" ++ unpack t
     OutdatedSolcVersion v  -> "Solc version " ++ toString v ++ " detected. Echidna doesn't support versions of solc before " ++ toString minSupportedSolcVersion ++ ". Please use a newer version."
 
diff --git a/lib/Echidna/Types/Tx.hs b/lib/Echidna/Types/Tx.hs
index e62d140df..722fa1ccd 100644
--- a/lib/Echidna/Types/Tx.hs
+++ b/lib/Echidna/Types/Tx.hs
@@ -197,6 +197,7 @@ data TxResult
   | ErrorReturnDataOutOfBounds
   | ErrorNonexistentFork
   | ErrorNonexistentPrecompile
+  | ErrorAssumeCheatFailed
   deriving (Eq, Ord, Show, Enum)
 $(deriveJSON defaultOptions ''TxResult)
 
@@ -263,6 +264,7 @@ getResult = \case
   VMFailure ReturnDataOutOfBounds         -> ErrorReturnDataOutOfBounds
   VMFailure (NonexistentFork _)           -> ErrorNonexistentFork
   VMFailure (NonexistentPrecompile _)     -> ErrorNonexistentPrecompile
+  VMFailure AssumeCheatFailed             -> ErrorAssumeCheatFailed
 
 makeSingleTx :: Addr -> Addr -> W256 -> TxCall -> [Tx]
 makeSingleTx a d v (SolCall c) = [Tx (SolCall c) a d maxGasPerBlock 0 v (0, 0)]
diff --git a/package.yaml b/package.yaml
index 422d6207e..d7e286948 100644
--- a/package.yaml
+++ b/package.yaml
@@ -116,6 +116,7 @@ tests:
     main: Spec.hs
     source-dirs: src/test
     dependencies:
+      - bytestring
       - data-dword
       - echidna
       - exceptions
diff --git a/src/Main.hs b/src/Main.hs
index 5e5c15cc9..50e866c79 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -193,7 +193,7 @@ options = Options . NE.fromList
     <> metavar "PATH"
     <> help "Directory to save coverage reports. Defaults to corpus-dir if not specified.")
   <*> optional (option str $ long "test-mode"
-    <> help "Test mode to use. Either 'property', 'assertion', 'dapptest', 'optimization', 'overflow' or 'exploration'" )
+    <> help "Test mode to use. Either 'property', 'assertion', 'foundry', 'optimization', 'overflow' or 'exploration'" )
   <*> switch (long "all-contracts"
     <> help "Generate calls to all deployed contracts.")
   <*> optional (option auto $ long "timeout"
diff --git a/src/test/Common.hs b/src/test/Common.hs
index a9cb7eb26..fc8ef8e79 100644
--- a/src/test/Common.hs
+++ b/src/test/Common.hs
@@ -5,6 +5,7 @@ module Common
   , testContractV
   , solcV
   , testContract'
+  , testContractNamed
   , checkConstructorConditions
   , optimized
   , solnFor
@@ -126,7 +127,19 @@ testContract'
   -> WorkerType
   -> [(String, (Env, WorkerState) -> IO Bool)]
   -> TestTree
-testContract' fp n v configPath s workerType expectations = testCase fp $ withSolcVersion v $ do
+testContract' fp = testContractNamed fp fp
+
+testContractNamed
+  :: String
+  -> FilePath
+  -> Maybe ContractName
+  -> Maybe SolcVersionComp
+  -> Maybe FilePath
+  -> Bool
+  -> WorkerType
+  -> [(String, (Env, WorkerState) -> IO Bool)]
+  -> TestTree
+testContractNamed name fp n v configPath s workerType expectations = testCase name $ withSolcVersion v $ do
   c <- case configPath of
     Just path -> do
       parsed <- parseConfig path
@@ -155,7 +168,7 @@ loadSolTests cfg buildOutput name = do
       eventMap = Map.unions $ map (.eventMap) contracts
       world = World solConf.sender mempty Nothing [] [] eventMap
   mainContract <- selectMainContract solConf name contracts
-  echidnaTests <- mkTests solConf mainContract
+  echidnaTests <- mkTests solConf cfg.campaignConf mainContract
   env <- mkEnv cfg buildOutput echidnaTests world Nothing
   vm <- loadSpecified env mainContract contracts
   pure (vm, env, echidnaTests)
diff --git a/src/test/Spec.hs b/src/test/Spec.hs
index a914c5def..8c17015ec 100644
--- a/src/test/Spec.hs
+++ b/src/test/Spec.hs
@@ -6,8 +6,8 @@ import Tests.Cheat (cheatTests)
 import Tests.Compile (compilationTests)
 import Tests.Config (configTests)
 import Tests.Coverage (coverageTests)
-import Tests.Dapptest (dapptestTests)
 import Tests.Encoding (encodingJSONTests)
+import Tests.Foundry (foundryTests)
 import Tests.FoundryTestGen (foundryTestGenTests)
 import Tests.Integration (integrationTests)
 import Tests.Optimization (optimizationTests)
@@ -31,7 +31,7 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $
            , overflowTests
            , optimizationTests
            , researchTests
-           , dapptestTests
+           , foundryTests
            , encodingJSONTests
            , foundryTestGenTests
            , cheatTests
diff --git a/src/test/Tests/Dapptest.hs b/src/test/Tests/Foundry.hs
similarity index 71%
rename from src/test/Tests/Dapptest.hs
rename to src/test/Tests/Foundry.hs
index 15839e7ad..60cac51ee 100644
--- a/src/test/Tests/Dapptest.hs
+++ b/src/test/Tests/Foundry.hs
@@ -1,14 +1,14 @@
-module Tests.Dapptest (dapptestTests) where
+module Tests.Foundry (foundryTests) where
 
 import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract', solcV, solved, passed)
 import Echidna.Types.Worker (WorkerType(..))
 
-dapptestTests :: TestTree
-dapptestTests = testGroup "Dapptest Integration Testing"
-  [ testContract' "dapptest/basic.sol" (Just "GreeterTest") (Just (\v -> v >= solcV (0,7,5))) (Just "dapptest/config.yaml") False FuzzWorker
-     [ 
+foundryTests :: TestTree
+foundryTests = testGroup "Foundry Integration Testing"
+  [ testContract' "foundry-basic/basic.sol" (Just "GreeterTest") (Just (\v -> v >= solcV (0,7,5))) (Just "foundry-basic/config.yaml") False FuzzWorker
+     [
         ("testShrinking passed", solved "testShrinking"),
         ("testFuzzFixedArray passed", solved "testFuzzFixedArray"),
         ("testFuzzVariableArray passed", solved "testFuzzVariableArray"),
@@ -16,7 +16,7 @@ dapptestTests = testGroup "Dapptest Integration Testing"
         ("testFuzzBytes14 passed", solved "testFuzzBytes14"),
         ("testFuzzBytes32 passed", solved "testFuzzBytes32"),
         ("testFuzzI256 passed", solved "testFuzzI256"),
-        ("testFuzzAbiCoderV2 passed", solved "testFuzzAbiCoderV2"), 
+        ("testFuzzAbiCoderV2 passed", solved "testFuzzAbiCoderV2"),
         ("testAssume failed", passed "testFuzzAssume")
       ]
   ]
diff --git a/src/test/Tests/FoundryTestGen.hs b/src/test/Tests/FoundryTestGen.hs
index d404e7fe9..86017229c 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -1,84 +1,309 @@
 module Tests.FoundryTestGen (foundryTestGenTests) where
 
 import Test.Tasty (TestTree, testGroup)
-import Test.Tasty.HUnit (testCase, assertFailure)
+import Test.Tasty.HUnit (assertBool, assertFailure, testCase)
 
 import Control.Exception (catch, SomeException)
-import Data.List (isInfixOf)
+import Data.ByteString qualified as BS
+import Data.List (isInfixOf, isPrefixOf)
 import Data.Text (pack, unpack, replace)
 import qualified Data.Text.Lazy as TL
 import System.Directory (getTemporaryDirectory, removePathForcibly, findExecutable, copyFile)
 import System.Exit (ExitCode(..))
+import System.IO.Unsafe (unsafePerformIO)
 import System.Process (readProcessWithExitCode)
+import Text.Read (readMaybe)
 
+import Common (solved, passed, testContract, testContractNamed)
+import Echidna.Types.Config (Env)
+import Echidna.Types.Campaign (WorkerState)
 import EVM.ABI (AbiValue(..))
-import Echidna.Types.Tx (Tx(..), TxCall(..))
 import Echidna.Output.Foundry (foundryTest)
 import Echidna.Types.Test (EchidnaTest(..), TestType(..), TestValue(..), TestState(..))
+import Echidna.Types.Tx (Tx(..), TxCall(..))
+import Echidna.Types.Worker (WorkerType(FuzzWorker, SymbolicWorker))
 
 foundryTestGenTests :: TestTree
 foundryTestGenTests = testGroup "Foundry test generation"
   [ testCase "compiles with forge" testForgeCompilation
   , testCase "correctly encodes bytes1" testBytes1Encoding
+  , testCase "fallback function syntax" testFallbackSyntax
+  , testCase "null bytes in arguments" testNullBytes
+  , testGroup "Concrete execution (fuzzing)"
+      [ testForgeStd "solves assertTrue"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertTrueTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertTrue should be detected concrete", solved "test_assert_true")
+          ]
+      , testForgeStd "solves assertFalse"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertFalseTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertFalse should be detected concrete", solved "test_assert_false")
+          ]
+      , testForgeStd "solves assertEq"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertEqTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertEq should be detected concrete", solved "test_assert_eq")
+          ]
+      , testForgeStd "solves assertNotEq"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertNotEqTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertNotEq should be detected concrete", solved "test_assert_not_eq")
+          ]
+      , testForgeStd "solves assertEqDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertEqDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertEqDecimal should be detected concrete", solved "test_assert_eq_decimal")
+          ]
+      , testForgeStd "solves assertNotEqDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertNotEqDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertNotEqDecimal should be detected concrete", solved "test_assert_not_eq_decimal")
+          ]
+      , testForgeStd "solves assertLt"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertLtTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLt should be detected concrete", solved "test_assert_lt")
+          ]
+      , testForgeStd "solves assertGt"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertGtTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGt should be detected concrete", solved "test_assert_gt")
+          ]
+      , testForgeStd "solves assertLtDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertLtDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLtDecimal should be detected concrete", solved "test_assert_lt_decimal")
+          ]
+      , testForgeStd "solves assertGtDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertGtDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGtDecimal should be detected concrete", solved "test_assert_gt_decimal")
+          ]
+      , testForgeStd "solves assertLe"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertLeTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLe should be detected concrete", solved "test_assert_le")
+          ]
+      , testForgeStd "solves assertGe"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertGeTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGe should be detected concrete", solved "test_assert_ge")
+          ]
+      , testForgeStd "solves assertLeDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertLeDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLeDecimal should be detected concrete", solved "test_assert_le_decimal")
+          ]
+      , testForgeStd "solves assertGeDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertGeDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGeDecimal should be detected concrete", solved "test_assert_ge_decimal")
+          ]
+      , testForgeStd "solves assertApproxEqAbs"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqAbsTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqAbs should be detected concrete", solved "test_assert_approx_eq_abs")
+          ]
+      , testForgeStd "solves assertApproxEqAbsDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqAbsDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqAbsDecimal should be detected concrete", solved "test_assert_approx_eq_abs_decimal")
+          ]
+      , testForgeStd "solves assertApproxEqRel"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqRelTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqRel should be detected concrete", solved "test_assert_approx_eq_rel")
+          ]
+      , testForgeStd "solves assertApproxEqRelDecimal"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqRelDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqRelDecimal should be detected concrete", solved "test_assert_approx_eq_rel_decimal")
+          ]
+      , testContract "foundry/StatelessBug.sol" (Just "foundry/StatelessBug.yaml")
+          [ ("stateless bug should be detected concrete", solved "checkValue")
+          ]
+      , testForgeStd "solves revert"
+          "foundry/FoundryAsserts.sol"
+          (Just "RevertTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("revert should be detected as failure concrete", solved "test_revert_is_failure")
+          ]
+      , testForgeStd "solves invariant"
+          "foundry/FoundryAsserts.sol"
+          (Just "InvariantTest") (Just "foundry/FoundryInvariant.yaml")
+          FuzzWorker
+          [ ("invariant should be detected with seqLen > 1", solved "invariant_counter_below_limit")
+          ]
+      , testForgeStd "vm.assume filters inputs"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssumeTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("vm.assume should not be treated as test failure", passed "test_assume_filters")
+          ]
+      ]
+  , testGroup "Symbolic execution (SMT solving)"
+      [ testForgeStd "solves assertTrue"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertTrueTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertTrue should be detected symbolic", solved "test_assert_true")
+          ]
+      , testForgeStd "solves assertFalse"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertFalseTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertFalse should be detected symbolic", solved "test_assert_false")
+          ]
+      , testForgeStd "solves assertEq"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertEqTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertEq should be detected symbolic", solved "test_assert_eq")
+          ]
+      , testForgeStd "solves assertNotEq"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertNotEqTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertNotEq should be detected symbolic", solved "test_assert_not_eq")
+          ]
+      , testForgeStd "solves assertLt"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertLtTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertLt should be detected symbolic", solved "test_assert_lt")
+          ]
+      , testForgeStd "solves assertGt"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertGtTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertGt should be detected symbolic", solved "test_assert_gt")
+          ]
+      , testForgeStd "solves assertLe"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertLeTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertLe should be detected symbolic", solved "test_assert_le")
+          ]
+      , testForgeStd "solves assertGe"
+          "foundry/FoundryAsserts.sol"
+          (Just "AssertGeTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertGe should be detected symbolic", solved "test_assert_ge")
+          ]
+      -- Note: The following assertions are NOT supported in symbolic execution
+      -- mode because hevm's symbolic execution engine doesn't recognize the
+      -- following cheatcodes:
+      -- - assertEqDecimal, assertNotEqDecimal
+      -- - assertLtDecimal, assertGtDecimal, assertLeDecimal, assertGeDecimal
+      -- - assertApproxEqAbs, assertApproxEqAbsDecimal
+      -- - assertApproxEqRel, assertApproxEqRelDecimal
+      -- These are only tested in concrete (fuzzing) mode above.
+      ]
+  , testGroup "Assertion mode with Foundry assertX"
+      [ testForgeStd "solves assertTrue in assertion mode"
+          "foundry/FoundryAssertsAssertionMode.sol"
+          (Just "FoundryAssertsAssertionModeTest") (Just "foundry/FoundryAssertsAssertionMode.yaml")
+          FuzzWorker
+          [ ("assertTrue should be detected in assertion mode", solved "check_assert_true")
+          ]
+      , testForgeStd "solves assertEq in assertion mode"
+          "foundry/FoundryAssertsAssertionMode.sol"
+          (Just "FoundryAssertsAssertionModeTest") (Just "foundry/FoundryAssertsAssertionMode.yaml")
+          FuzzWorker
+          [ ("assertEq should be detected in assertion mode", solved "check_assert_eq")
+          ]
+      , testForgeStd "solves assertGt in assertion mode"
+          "foundry/FoundryAssertsAssertionMode.sol"
+          (Just "FoundryAssertsAssertionModeTest") (Just "foundry/FoundryAssertsAssertionMode.yaml")
+          FuzzWorker
+          [ ("assertGt should be detected in assertion mode", solved "check_assert_gt")
+          ]
+      ]
   ]
 
 -- | Verify generated test compiles with forge.
+testForgeCompilation :: IO ()
+testForgeCompilation =
+  testForgeCompiles "forge-compilation-test" "FoundryTestTarget" mkMinimalTest "Generated.t.sol"
+
+-- | Test that generated test with fallback function call compiles with forge.
+testFallbackSyntax :: IO ()
+testFallbackSyntax =
+  let fallbackTest = mkMinimalTest
+        { reproducer = [Tx (SolCall ("", [])) 0 0 0 0 0 (0, 0)] }
+  in testForgeCompiles "forge-fallback-test" "FallbackTest" fallbackTest "FallbackGenerated.t.sol"
+
+-- | Test that generated test with null bytes in arguments compiles with forge.
+testNullBytes :: IO ()
+testNullBytes =
+  let nullByteData = BS.pack [0x00, 0x01, 0x00, 0x02, 0x00, 0x00, 0x03]  -- Mix of null and non-null bytes
+      nullByteArg = AbiBytes 32 (nullByteData <> BS.replicate (32 - BS.length nullByteData) 0)
+      nullByteTest = mkMinimalTest
+        { reproducer = [Tx (SolCall ("checkBytes", [nullByteArg])) 0 0 0 0 0 (0, 0)] }
+  in testForgeCompiles "forge-nullbyte-test" "NullByteTest" nullByteTest "NullByteGenerated.t.sol"
+
+-- | Helper function to test that generated Foundry code compiles with forge.
+-- Takes a test description, contract name, test data, and output file name.
 -- We use temp directories because we need to test the full forge workflow:
 -- forge init (for dependencies) + our generated test + forge build.
-testForgeCompilation :: IO ()
-testForgeCompilation = do
+testForgeCompiles :: String -> String -> EchidnaTest -> String -> IO ()
+testForgeCompiles tmpDirSuffix contractName testData outputFile = do
   forgeExe <- findExecutable "forge"
   case forgeExe of
-    Nothing -> 
+    Nothing ->
       assertFailure "forge not found"
     Just _ -> do
       tmpBase <- getTemporaryDirectory
-      let tmpDir = tmpBase ++ "/echidna-forge-test"
-      
+      let tmpDir = tmpBase ++ "/echidna-" ++ tmpDirSuffix
+          contractFile = contractName ++ ".sol"
+          contractPath = "foundry/" ++ contractFile
+
       catch (removePathForcibly tmpDir) (\(_ :: SomeException) -> pure ())
-      
+
       -- Initialize project with forge.
       (code, _, err) <- readProcessWithExitCode "forge" ["init", tmpDir] ""
       if code /= ExitSuccess
         then assertFailure $ "forge init failed: " ++ err
         else do
-          copyFile "foundry/FoundryTestTarget.sol" (tmpDir ++ "/src/FoundryTestTarget.sol")
-          
-          -- Simulate user action: Replace the target contract with the actual
-          -- contract instance and import it (add contract import after the
-          -- forge-std one).
-          let generated = TL.unpack $ foundryTest (Just "FoundryTestTarget") mkMinimalTest
+          copyFile contractPath (tmpDir ++ "/src/" ++ contractFile)
+
+          -- Generate test and add contract import after forge-std import
+          let generated = TL.unpack $ foundryTest (Just (pack contractName)) testData
               forgeStdImport = pack "import \"forge-std/Test.sol\";"
-              contractImport = pack "import \"../src/FoundryTestTarget.sol\";"
-              testWithImport = unpack $ replace forgeStdImport 
-                                               (forgeStdImport <> "\n" <> contractImport) 
+              contractImport = pack $ "import \"../src/" ++ contractFile ++ "\";"
+              testWithImport = unpack $ replace forgeStdImport
+                                               (forgeStdImport <> "\n" <> contractImport)
                                                (pack generated)
-          
-          writeFile (tmpDir ++ "/test/Generated.t.sol") testWithImport
-          
+
+          writeFile (tmpDir ++ "/test/" ++ outputFile) testWithImport
+
           (buildCode, _, buildErr) <- readProcessWithExitCode "forge" ["build", "--root", tmpDir] ""
-          
+
           catch (removePathForcibly tmpDir) (\(_ :: SomeException) -> pure ())
-          
+
           if buildCode == ExitSuccess
             then pure ()
             else assertFailure $ "forge build failed: " ++ buildErr
 
-mkMinimalTest :: EchidnaTest
-mkMinimalTest = EchidnaTest
-  -- Foundry tests are only generated for solved/large tests.
-  { state = Large 0
-  -- AssertionTest is required for Foundry test generation.
-  , testType = AssertionTest False ("test", []) 0
-  , value = BoolValue True
-  -- Empty reproducer is sufficient for testing contract name generation.
-  , reproducer = []
-  -- These fields are not read by the output generator.
-  , result = error "result not needed for Foundry output tests"
-  , vm = Nothing
-  , workerId = Nothing
-  }
-
 testBytes1Encoding :: IO ()
 testBytes1Encoding = do
   let
@@ -97,3 +322,59 @@ testBytes1Encoding = do
   if "hex\"92\"" `isInfixOf` generated
     then pure ()
     else assertFailure $ "bytes1 not correctly encoded: " ++ generated
+
+-- | Wrapper for testContractNamed that skips if solc < 0.8.13.
+testForgeStd :: String -> FilePath -> Maybe String -> Maybe FilePath -> WorkerType -> [(String, (Env, WorkerState) -> IO Bool)] -> TestTree
+testForgeStd name fp contract config workerType checks =
+  if solcSupportsForgeStd
+    then testContractNamed name fp (pack <$> contract) Nothing config True workerType checks
+    else testCase name $ assertBool "skip (solc < 0.8.13, forge-std requires >= 0.8.13)" True
+
+-- | Check if solc >= 0.8.13 (required for forge-std). Computed once on module
+-- load. This is used to skip tests that require forge-std if solc is too old.
+{-# NOINLINE solcSupportsForgeStd #-}
+solcSupportsForgeStd :: Bool
+solcSupportsForgeStd = unsafePerformIO $ do
+  result <- findExecutable "solc"
+  case result of
+    Nothing -> pure False
+    Just _ -> do
+      (code, out, _) <- readProcessWithExitCode "solc" ["--version"] ""
+      pure $ code == ExitSuccess && maybe False (>= (0, 8, 13)) (parseSolcVersion out)
+  where
+    parseSolcVersion :: String -> Maybe (Int, Int, Int)
+    parseSolcVersion output =
+      case filter ("Version:" `isPrefixOf`) (lines output) of
+        (line:_) ->
+          let versionPart = dropWhile (/= ':') line
+              version = takeWhile (/= '+') $ drop 2 versionPart
+              parts = words version
+          in case parts of
+               (v:_) -> parseVersion v
+               _ -> Nothing
+        _ -> Nothing
+
+    parseVersion :: String -> Maybe (Int, Int, Int)
+    parseVersion v = case map readMaybe (splitOn '.' v) of
+      [Just major, Just minor, Just patch] -> Just (major, minor, patch)
+      _ -> Nothing
+
+    splitOn :: Char -> String -> [String]
+    splitOn c s = case break (== c) s of
+      (a, _:b) -> a : splitOn c b
+      (a, [])  -> [a]
+
+mkMinimalTest :: EchidnaTest
+mkMinimalTest = EchidnaTest
+  -- Foundry tests are only generated for solved/large tests.
+  { state = Large 0
+  -- AssertionTest is required for Foundry test generation.
+  , testType = AssertionTest False ("test", []) 0
+  , value = BoolValue True
+  -- Empty reproducer is sufficient for testing contract name generation.
+  , reproducer = []
+  -- These fields are not read by the output generator.
+  , result = error "result not needed for Foundry output tests"
+  , vm = Nothing
+  , workerId = Nothing
+  }
\ No newline at end of file
diff --git a/stack.yaml b/stack.yaml
index 035015722..964227c6f 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: https://github.com/argotorg/hevm.git
-  commit: 41e6d1304411749ea8c816d131991663b5dca67a
+  commit: ed90053fa0ed69e658a75ab0ed64d467f5a5448d
 
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162
diff --git a/tests/solidity/dapptest/basic.sol b/tests/solidity/foundry-basic/basic.sol
similarity index 83%
rename from tests/solidity/dapptest/basic.sol
rename to tests/solidity/foundry-basic/basic.sol
index 572c2efc0..612e6e362 100644
--- a/tests/solidity/dapptest/basic.sol
+++ b/tests/solidity/foundry-basic/basic.sol
@@ -2,6 +2,11 @@
 pragma abicoder v2;
 pragma solidity >=0.7.5;
 
+// Minimal Vm interface (this contract doesn't use forge-std).
+interface Vm {
+    function assume(bool condition) external pure;
+}
+
 contract Greeter {
     string public greeting;
 
@@ -85,7 +90,9 @@ contract GreeterTest is GreeterTestSetup {
     }
 
     function testFuzzAssume(uint256 x) public {
-        require(false, "FOUNDRY::ASSUME");
-        // unreachable
+        // keccak256("hevm cheat code") - standard hevm cheatcode address
+        // https://github.com/argotorg/hevm/blob/ed90053fa0ed69e658a75ab0ed64d467f5a5448d/src/EVM.hs#L1861
+        Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D).assume(x <= 100);
+        assert(x <= 100);
     }
 }
diff --git a/tests/solidity/dapptest/config.yaml b/tests/solidity/foundry-basic/config.yaml
similarity index 69%
rename from tests/solidity/dapptest/config.yaml
rename to tests/solidity/foundry-basic/config.yaml
index 6ce1300dd..328392dea 100644
--- a/tests/solidity/dapptest/config.yaml
+++ b/tests/solidity/foundry-basic/config.yaml
@@ -1,4 +1,4 @@
-testMode: dapptest
+testMode: foundry
 testLimit: 5000
 shrinkLimit: 100
 seqLen: 1
diff --git a/tests/solidity/foundry/FallbackTest.sol b/tests/solidity/foundry/FallbackTest.sol
new file mode 100644
index 000000000..9211bbd47
--- /dev/null
+++ b/tests/solidity/foundry/FallbackTest.sol
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract FallbackTest {
+    uint256 public fallbackCalled = 0;
+
+    // Fallback function
+    fallback() external {
+        fallbackCalled++;
+        // This should fail when fallback is called
+        assert(fallbackCalled == 0);
+    }
+}
+
diff --git a/tests/solidity/foundry/FoundryAsserts.sol b/tests/solidity/foundry/FoundryAsserts.sol
new file mode 100644
index 000000000..14f752372
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAsserts.sol
@@ -0,0 +1,170 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "forge-std/Test.sol";
+
+// Test contracts for Foundry's assertX functions detection
+
+contract AssertTrueTest is Test {
+    // This assertion can be broken when x > 100
+    function test_assert_true(uint256 x) public pure {
+        assertTrue(x <= 100);
+    }
+}
+
+contract AssertFalseTest is Test {
+    // This assertion can be broken when x > 100
+    function test_assert_false(uint256 x) public pure {
+        assertFalse(x > 100);
+    }
+}
+
+contract AssertEqTest is Test {
+    // This assertion can be broken when x != y
+    function test_assert_eq(uint256 x, uint256 y) public pure {
+        assertEq(x, y);
+    }
+}
+
+contract AssertNotEqTest is Test {
+    // This assertion can be broken when x == y
+    function test_assert_not_eq(uint256 x, uint256 y) public pure {
+        assertNotEq(x, y);
+    }
+}
+
+contract AssertEqDecimalTest is Test {
+    // This assertion can be broken when x != y
+    function test_assert_eq_decimal(uint256 x, uint256 y) public pure {
+        assertEqDecimal(x, y, 1);
+    }
+}
+
+contract AssertNotEqDecimalTest is Test {
+    // This assertion can be broken when x == y
+    function test_assert_not_eq_decimal(uint256 x, uint256 y) public pure {
+        assertNotEqDecimal(x, y, 1);
+    }
+}
+
+contract AssertLtTest is Test {
+    // This assertion can be broken when x >= y
+    function test_assert_lt(uint256 x, uint256 y) public pure {
+        assertLt(x, y);
+    }
+}
+
+contract AssertGtTest is Test {
+    // This assertion can be broken when x <= y
+    function test_assert_gt(uint256 x, uint256 y) public pure {
+        assertGt(x, y);
+    }
+}
+
+contract AssertLtDecimalTest is Test {
+    // This assertion can be broken when x >= y
+    function test_assert_lt_decimal(uint256 x, uint256 y) public pure {
+        assertLtDecimal(x, y, 1);
+    }
+}
+
+contract AssertGtDecimalTest is Test {
+    // This assertion can be broken when x <= y
+    function test_assert_gt_decimal(uint256 x, uint256 y) public pure {
+        assertGtDecimal(x, y, 1);
+    }
+}
+
+contract AssertLeTest is Test {
+    // This assertion can be broken when x > y
+    function test_assert_le(uint256 x, uint256 y) public pure {
+        assertLe(x, y);
+    }
+}
+
+contract AssertGeTest is Test {
+    // This assertion can be broken when x < y
+    function test_assert_ge(uint256 x, uint256 y) public pure {
+        assertGe(x, y);
+    }
+}
+
+contract AssertLeDecimalTest is Test {
+    // This assertion can be broken when x > y
+    function test_assert_le_decimal(uint256 x, uint256 y) public pure {
+        assertLeDecimal(x, y, 1);
+    }
+}
+
+contract AssertGeDecimalTest is Test {
+    // This assertion can be broken when x < y
+    function test_assert_ge_decimal(uint256 x, uint256 y) public pure {
+        assertGeDecimal(x, y, 1);
+    }
+}
+
+contract AssertApproxEqAbsTest is Test {
+    // This assertion can be broken when |x - y| > 1
+    function test_assert_approx_eq_abs(uint256 x, uint256 y) public pure {
+        // Allowing 1 unit of difference between x and y
+        assertApproxEqAbs(x, y, 1);
+    }
+}
+
+contract AssertApproxEqAbsDecimalTest is Test {
+    // This assertion can be broken when |x - y| > 100 (with 1 decimal
+    // precision)
+    function test_assert_approx_eq_abs_decimal(uint256 x, uint256 y) public pure {
+        assertApproxEqAbsDecimal(x, y, 100, 1);
+    }
+}
+
+contract AssertApproxEqRelTest is Test {
+    // This assertion can be broken when percentage delta > 1%
+    // Note: 1e18 = 100%, so 0.01e18 = 1%
+    function test_assert_approx_eq_rel(uint256 x, uint256 y) public pure {
+        assertApproxEqRel(x, y, 0.01e18); // 1% tolerance
+    }
+}
+
+contract AssertApproxEqRelDecimalTest is Test {
+    // This assertion can be broken when percentage delta > 1% (formatted with
+    // 1 decimal precision)
+    // Note: 1e18 = 100%, so 0.01e18 = 1%
+    function test_assert_approx_eq_rel_decimal(uint256 x, uint256 y) public pure {
+        assertApproxEqRelDecimal(x, y, 0.01e18, 1); // 1% tolerance
+    }
+}
+
+contract InvariantTest is Test {
+    uint256 public counter;
+
+    // State-mutating function called during sequences
+    function increase(uint256 x) public {
+        counter += x;
+    }
+
+    // Invariant that can be violated when counter > 100
+    function invariant_counter_below_limit() public view {
+        assertTrue(counter <= 5);
+    }
+}
+
+contract RevertTest is Test {
+    // Explicit reverts should be detected as test failures
+    function test_revert_is_failure(uint256 x) public pure {
+        if (x > 100) {
+            revert("Value too large");
+        }
+    }
+}
+
+contract AssumeTest is Test {
+    // vm.assume should filter inputs without counting as a test failure.
+    // When x > 100, vm.assume(false) triggers AssumeCheatFailed which
+    // echidna should ignore. The assertion always holds for accepted inputs
+    function test_assume_filters(uint256 x) public pure {
+        vm.assume(x <= 100);
+        assertTrue(x <= 100);
+    }
+}
\ No newline at end of file
diff --git a/tests/solidity/foundry/FoundryAsserts.yaml b/tests/solidity/foundry/FoundryAsserts.yaml
new file mode 100644
index 000000000..e1c90df7c
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAsserts.yaml
@@ -0,0 +1,4 @@
+testMode: foundry
+seed: 1234
+cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
+disableSlither: true
diff --git a/tests/solidity/foundry/FoundryAssertsAssertionMode.sol b/tests/solidity/foundry/FoundryAssertsAssertionMode.sol
new file mode 100644
index 000000000..7322a4159
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAssertsAssertionMode.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "forge-std/Test.sol";
+
+// Test that Foundry's assertX functions trigger failures in assertion mode.
+// In assertion mode, ALL functions are checked (no test_ prefix needed).
+contract FoundryAssertsAssertionModeTest is Test {
+    // This assertion can be broken when x > 100
+    function check_assert_true(uint256 x) public pure {
+        assertTrue(x <= 100);
+    }
+
+    // This assertion can be broken when x != y
+    function check_assert_eq(uint256 x, uint256 y) public pure {
+        assertEq(x, y);
+    }
+
+    // This assertion can be broken when x <= y
+    function check_assert_gt(uint256 x, uint256 y) public pure {
+        assertGt(x, y);
+    }
+
+    // This function should never fail
+    function safe_function(uint256 x) public pure {
+        uint256 y = x + 0;
+        require(y == x);
+    }
+}
diff --git a/tests/solidity/foundry/FoundryAssertsAssertionMode.yaml b/tests/solidity/foundry/FoundryAssertsAssertionMode.yaml
new file mode 100644
index 000000000..1b223cf70
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAssertsAssertionMode.yaml
@@ -0,0 +1,4 @@
+testMode: assertion
+seed: 1234
+cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
+disableSlither: true
diff --git a/tests/solidity/foundry/FoundryAssertsSymbolic.yaml b/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
new file mode 100644
index 000000000..ea114f0f2
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
@@ -0,0 +1,8 @@
+testMode: foundry
+seed: 1234
+cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
+symExec: true
+symExecSMTSolver: bitwuzla
+workers: 0
+seqLen: 1
+disableSlither: true
diff --git a/tests/solidity/foundry/FoundryInvariant.yaml b/tests/solidity/foundry/FoundryInvariant.yaml
new file mode 100644
index 000000000..e1c90df7c
--- /dev/null
+++ b/tests/solidity/foundry/FoundryInvariant.yaml
@@ -0,0 +1,4 @@
+testMode: foundry
+seed: 1234
+cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
+disableSlither: true
diff --git a/tests/solidity/foundry/NullByteTest.sol b/tests/solidity/foundry/NullByteTest.sol
new file mode 100644
index 000000000..eb2f1dcd7
--- /dev/null
+++ b/tests/solidity/foundry/NullByteTest.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract NullByteTest {
+    // Simple function that takes bytes32 parameter
+    function checkBytes(bytes32 data) public pure returns (bool) {
+        return data != bytes32(0);
+    }
+}
diff --git a/tests/solidity/foundry/StatelessBug.sol b/tests/solidity/foundry/StatelessBug.sol
new file mode 100644
index 000000000..6b4cbc4ce
--- /dev/null
+++ b/tests/solidity/foundry/StatelessBug.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// Simple stateless contract with an assertion that can be broken
+contract StatelessBuggy {
+    // This assertion can be broken when x > 100
+    function checkValue(uint256 x) public pure {
+        assert(x <= 100);
+    }
+}
diff --git a/tests/solidity/foundry/StatelessBug.yaml b/tests/solidity/foundry/StatelessBug.yaml
new file mode 100644
index 000000000..a47057f91
--- /dev/null
+++ b/tests/solidity/foundry/StatelessBug.yaml
@@ -0,0 +1,3 @@
+testMode: assertion
+seed: 1234
+disableSlither: true
diff --git a/tests/solidity/foundry/forge-std b/tests/solidity/foundry/forge-std
new file mode 160000
index 000000000..52965365c
--- /dev/null
+++ b/tests/solidity/foundry/forge-std
@@ -0,0 +1 @@
+Subproject commit 52965365cb81caa384c44ba2129e36a2e82bde85
diff --git a/tests/solidity/foundry/remappings.txt b/tests/solidity/foundry/remappings.txt
new file mode 100644
index 000000000..21843cd8a
--- /dev/null
+++ b/tests/solidity/foundry/remappings.txt
@@ -0,0 +1 @@
+forge-std/=forge-std/src/