From 67f67f8bc77d6ee1e4e10cd4097b2ace277f53b8 Mon Sep 17 00:00:00 2001
From: gustavo-grieco <gustavo.grieco+github@gmail.com>
Date: Tue, 16 Dec 2025 16:35:20 +0100
Subject: [PATCH 01/17] improved support for foundry tests

---
 lib/Echidna/Solidity.hs       |  3 ++-
 lib/Echidna/SymExec/Common.hs | 27 +++++++++++++++++++++++++--
 lib/Echidna/Test.hs           |  2 ++
 3 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index fd27b061c..e23e8cb4d 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -223,7 +223,7 @@ 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
 
@@ -233,6 +233,7 @@ loadSpecified env mainContract cs = do
 
   where
     setUpFunction = ("setUp", [])
+    is_testFunction = ("IS_TEST", [])
 
 
 selectMainContract
diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index 5731e8801..b20413450 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -2,24 +2,29 @@ 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.Function ((&))
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text qualified as T
+import Data.List (foldl')
 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.Solvers (SolverGroup)
-import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), checkAssertions, subModel, defaultSymbolicValues)
+import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
 import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
+import EVM.Types (EvmError(..), )
 import qualified EVM.Types (VM(..))
 
 import Echidna.Types (fromEVM)
@@ -27,6 +32,24 @@ 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)
+
+checkAssertions :: [Word256] -> Postcondition
+checkAssertions errs _ = \case
+  Failure _ _ (UnrecognizedOpcode 0xfe)  -> PBool False
+  Failure _ _ (Revert msg) -> case msg of
+    ConcreteBuf b ->
+      -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
+      let assertFail = (selector "Error(string)" `BS.isPrefixOf` b) &&
+            ("assertion failed" `BS.isPrefixOf` (BS.drop txtOffset b))
+      in if assertFail || b == panicMsg 0x01 then PBool False
+      else PBool True
+    _ -> error "Non-concrete revert message in assertion check"
+  _ -> PBool True
+  where
+    txtOffset = 4+32+32 -- selector + offset + length
+
 type PartialsLogs = [T.Text]
 
 data TxOrError = TxFromResult Tx | SMTErrorFromResult String
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index fb13c636e..14c84faff 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -215,7 +215,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

From e1f3265ba552a877cdf64c022b9db66f059b073c Mon Sep 17 00:00:00 2001
From: Radu Bahmata <92028479+BowTiedRadone@users.noreply.github.com>
Date: Tue, 13 Jan 2026 14:45:14 +0200
Subject: [PATCH 02/17] Extend Foundry support testing (#1512)

---
 .gitmodules                                   |   3 +
 lib/Echidna/SymExec/Common.hs                 |  26 +-
 package.yaml                                  |   1 +
 src/test/Tests/FoundryTestGen.hs              | 228 +++++++++++++++++-
 tests/solidity/foundry/FoundryAsserts.sol     | 146 +++++++++++
 tests/solidity/foundry/FoundryAsserts.yaml    |   3 +
 .../foundry/FoundryAssertsSymbolic.yaml       |   7 +
 tests/solidity/foundry/StatelessBug.sol       |  10 +
 tests/solidity/foundry/StatelessBug.yaml      |   2 +
 tests/solidity/foundry/forge-std              |   1 +
 tests/solidity/foundry/remappings.txt         |   1 +
 11 files changed, 406 insertions(+), 22 deletions(-)
 create mode 100644 .gitmodules
 create mode 100644 tests/solidity/foundry/FoundryAsserts.sol
 create mode 100644 tests/solidity/foundry/FoundryAsserts.yaml
 create mode 100644 tests/solidity/foundry/FoundryAssertsSymbolic.yaml
 create mode 100644 tests/solidity/foundry/StatelessBug.sol
 create mode 100644 tests/solidity/foundry/StatelessBug.yaml
 create mode 160000 tests/solidity/foundry/forge-std
 create mode 100644 tests/solidity/foundry/remappings.txt

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/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index b20413450..e07987838 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+
 module Echidna.SymExec.Common where
 
 import Control.Monad.IO.Unlift (MonadUnliftIO, liftIO)
@@ -11,7 +13,6 @@ import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text qualified as T
-import Data.List (foldl')
 import Optics.Core ((.~), (%), (%~))
 
 import EVM (loadContract, resetState, symbolify)
@@ -36,17 +37,18 @@ panicMsg :: Word256 -> ByteString
 panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
 
 checkAssertions :: [Word256] -> Postcondition
-checkAssertions errs _ = \case
-  Failure _ _ (UnrecognizedOpcode 0xfe)  -> PBool False
-  Failure _ _ (Revert msg) -> case msg of
-    ConcreteBuf b ->
-      -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
-      let assertFail = (selector "Error(string)" `BS.isPrefixOf` b) &&
-            ("assertion failed" `BS.isPrefixOf` (BS.drop txtOffset b))
-      in if assertFail || b == panicMsg 0x01 then PBool False
-      else PBool True
-    _ -> error "Non-concrete revert message in assertion check"
-  _ -> PBool True
+checkAssertions _ _ vmres =
+  case vmres of
+    Failure _ _ (UnrecognizedOpcode 0xfe) -> PBool False
+    Failure _ _ (Revert msg) -> case msg of
+      ConcreteBuf b ->
+        -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
+        let assertFail = (selector "Error(string)" `BS.isPrefixOf` b) &&
+              ("assertion failed" `BS.isPrefixOf` BS.drop txtOffset b)
+        in if assertFail || b == panicMsg 0x01 then PBool False
+        else PBool True
+      _ -> error "Non-concrete revert message in assertion check"
+    _ -> PBool True
   where
     txtOffset = 4+32+32 -- selector + offset + length
 
diff --git a/package.yaml b/package.yaml
index 6e519db4b..81706df10 100644
--- a/package.yaml
+++ b/package.yaml
@@ -119,6 +119,7 @@ tests:
       - data-dword
       - echidna
       - exceptions
+      - filepath
       - optics-core
       - process
       - semver
diff --git a/src/test/Tests/FoundryTestGen.hs b/src/test/Tests/FoundryTestGen.hs
index a67aa4499..7e9c2f584 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -10,12 +10,220 @@ import System.Directory (getTemporaryDirectory, removePathForcibly, findExecutab
 import System.Exit (ExitCode(..))
 import System.Process (readProcessWithExitCode)
 
+import Common (testContract, testContract', solved)
 import Echidna.Output.Foundry (foundryTest)
 import Echidna.Types.Test (EchidnaTest(..), TestType(..), TestValue(..), TestState(..))
+import Echidna.Types.Worker (WorkerType(FuzzWorker, SymbolicWorker))
 
 foundryTestGenTests :: TestTree
 foundryTestGenTests = testGroup "Foundry test generation"
   [ testCase "compiles with forge" testForgeCompilation
+  , testGroup "Concrete execution (fuzzing)"
+      [ testGroup "assertTrue"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertTrueTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_true")
+              ]
+          ]
+      , testGroup "assertFalse"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertFalseTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_false")
+              ]
+          ]
+      , testGroup "assertEq"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertEqTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_eq")
+              ]
+          ]
+      , testGroup "assertNotEq"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertNotEqTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_not_eq")
+              ]
+          ]
+      , testGroup "assertEqDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertEqDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_eq_decimal")
+              ]
+          ]
+      , testGroup "assertNotEqDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertNotEqDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_not_eq_decimal")
+              ]
+          ]
+      , testGroup "assertLt"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertLtTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_lt")
+              ]
+          ]
+      , testGroup "assertGt"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertGtTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_gt")
+              ]
+          ]
+      , testGroup "assertLtDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertLtDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_lt_decimal")
+              ]
+          ]
+      , testGroup "assertGtDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertGtDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_gt_decimal")
+              ]
+          ]
+      , testGroup "assertLe"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertLeTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_le")
+              ]
+          ]
+      , testGroup "assertGe"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertGeTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_ge")
+              ]
+          ]
+      , testGroup "assertLeDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertLeDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_le_decimal")
+              ]
+          ]
+      , testGroup "assertGeDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertGeDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_ge_decimal")
+              ]
+          ]
+      , testGroup "assertApproxEqAbs"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertApproxEqAbsTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_approx_eq_abs")
+              ]
+          ]
+      , testGroup "assertApproxEqAbsDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertApproxEqAbsDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_approx_eq_abs_decimal")
+              ]
+          ]
+      , testGroup "assertApproxEqRel"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertApproxEqRelTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_approx_eq_rel")
+              ]
+          ]
+      , testGroup "assertApproxEqRelDecimal"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertApproxEqRelDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected", solved "test_assert_approx_eq_rel_decimal")
+              ]
+          ]
+      , testGroup "stateless bug"
+          [ testContract "foundry/StatelessBug.sol" (Just "foundry/StatelessBug.yaml")
+              [ ("should be detected", solved "checkValue")
+              ]
+          ]
+      , testGroup "revert"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "RevertTest") Nothing (Just "foundry/FoundryAsserts.yaml")
+              True FuzzWorker
+              [ ("should be detected as failure", solved "test_revert_is_failure")
+              ]
+          ]
+      ]
+  , testGroup "Symbolic execution (SMT solving)"
+      [ testGroup "assertTrue"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertTrueTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_true")
+              ]
+          ]
+      , testGroup "assertFalse"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertFalseTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_false")
+              ]
+          ]
+      , testGroup "assertEq"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertEqTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_eq")
+              ]
+          ]
+      , testGroup "assertNotEq"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertNotEqTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_not_eq")
+              ]
+          ]
+      , testGroup "assertLt"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertLtTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_lt")
+              ]
+          ]
+      , testGroup "assertGt"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertGtTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_gt")
+              ]
+          ]
+      , testGroup "assertLe"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertLeTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", solved "test_assert_le")
+              ]
+          ]
+      , testGroup "assertGe"
+          [ testContract' "foundry/FoundryAsserts.sol"
+              (Just "AssertGeTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
+              True SymbolicWorker
+              [ ("should be detected", 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.
+      ]
   ]
 
 -- | Verify generated test compiles with forge.
@@ -25,37 +233,37 @@ testForgeCompilation :: IO ()
 testForgeCompilation = do
   forgeExe <- findExecutable "forge"
   case forgeExe of
-    Nothing -> 
+    Nothing ->
       assertFailure "forge not found"
     Just _ -> do
       tmpBase <- getTemporaryDirectory
       let tmpDir = tmpBase ++ "/echidna-forge-test"
-      
+
       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
               forgeStdImport = pack "import \"forge-std/Test.sol\";"
               contractImport = pack "import \"../src/FoundryTestTarget.sol\";"
-              testWithImport = unpack $ replace forgeStdImport 
-                                               (forgeStdImport <> "\n" <> contractImport) 
+              testWithImport = unpack $ replace forgeStdImport
+                                               (forgeStdImport <> "\n" <> contractImport)
                                                (pack generated)
-          
+
           writeFile (tmpDir ++ "/test/Generated.t.sol") testWithImport
-          
+
           (buildCode, _, buildErr) <- readProcessWithExitCode "forge" ["build", "--root", tmpDir] ""
-          
+
           catch (removePathForcibly tmpDir) (\(_ :: SomeException) -> pure ())
-          
+
           if buildCode == ExitSuccess
             then pure ()
             else assertFailure $ "forge build failed: " ++ buildErr
diff --git a/tests/solidity/foundry/FoundryAsserts.sol b/tests/solidity/foundry/FoundryAsserts.sol
new file mode 100644
index 000000000..3b99cc435
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAsserts.sol
@@ -0,0 +1,146 @@
+// 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 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");
+        }
+    }
+}
\ 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..0e6e2696b
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAsserts.yaml
@@ -0,0 +1,3 @@
+testMode: dapptest
+seed: 1234
+cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
diff --git a/tests/solidity/foundry/FoundryAssertsSymbolic.yaml b/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
new file mode 100644
index 000000000..58bc37a63
--- /dev/null
+++ b/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
@@ -0,0 +1,7 @@
+testMode: dapptest
+seed: 1234
+cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
+symExec: true
+symExecSMTSolver: bitwuzla
+workers: 0
+seqLen: 1
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..a21e7bb13
--- /dev/null
+++ b/tests/solidity/foundry/StatelessBug.yaml
@@ -0,0 +1,2 @@
+testMode: assertion
+seed: 1234
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/

From 00a8cfff7545637051781a7c6e9b274467ead58d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Wed, 14 Jan 2026 20:36:39 -0300
Subject: [PATCH 03/17] Fix lint failures

---
 lib/Echidna/SymExec/Common.hs | 3 +--
 lib/Echidna/Test.hs           | 2 +-
 package.yaml                  | 1 -
 3 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index e07987838..3ed15922e 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -24,8 +24,7 @@ import EVM.Format (formatPartialDetailed)
 import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData(..))
 import EVM.Solvers (SolverGroup)
 import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
-import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
-import EVM.Types (EvmError(..), )
+import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed, EvmError(..))
 import qualified EVM.Types (VM(..))
 
 import Echidna.Types (fromEVM)
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index 14c84faff..4d781a88c 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -215,7 +215,7 @@ 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))
+      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.
diff --git a/package.yaml b/package.yaml
index 81706df10..6e519db4b 100644
--- a/package.yaml
+++ b/package.yaml
@@ -119,7 +119,6 @@ tests:
       - data-dword
       - echidna
       - exceptions
-      - filepath
       - optics-core
       - process
       - semver

From 5659734274ec5f73ecdfb671823e66029338de4f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Wed, 14 Jan 2026 22:22:47 -0300
Subject: [PATCH 04/17] ci: bump python version to 3.10, clone submodules

---
 .github/workflows/ci.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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

From e3328ba0ee8fdc8bc9c304610a3723c5c6348990 Mon Sep 17 00:00:00 2001
From: gustavo-grieco <gustavo.grieco+github@gmail.com>
Date: Sat, 17 Jan 2026 16:22:26 +0100
Subject: [PATCH 05/17] some fixes when using foundry mode

---
 lib/Echidna/Campaign.hs             | 2 ++
 lib/Echidna/Solidity.hs             | 4 ++--
 lib/Echidna/SymExec/Common.hs       | 9 +++++----
 lib/Echidna/SymExec/Verification.hs | 1 +
 lib/Echidna/Test.hs                 | 6 +++---
 lib/Echidna/Types/Solidity.hs       | 4 ++--
 6 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 0543822f6..ec81bbe86 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -288,6 +288,8 @@ runSymWorker callback vm dict workerId _ name = do
     lift callback
 
     (symTxs, partials) <- liftIO $ takeMVar symTxsChan
+    liftIO $ print symTxs
+    liftIO $ print partials
     let txs = extractTxs symTxs
     let errors = extractErrors symTxs
 
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index e23e8cb4d..8664bd34d 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -149,7 +149,7 @@ filterMethods contractName (Blacklist ig) ms =
 -- | Filter methods with arguments, used for dapptest mode
 filterMethodsWithArgs :: NonEmpty SolSignature -> NonEmpty SolSignature
 filterMethodsWithArgs ms =
-  case NE.filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ms of
+  case NE.filter (\(n, xs) -> T.isPrefixOf "test" n && (T.isPrefixOf "invariant_" n || not (null xs))) ms of
     [] -> error "No dapptest tests found"
     fs -> NE.fromList fs
 
@@ -228,7 +228,7 @@ loadSpecified env mainContract cs = do
               else pure vm3
 
     case vm4.result of
-      Just (VMFailure _) -> throwM SetUpCallFailed
+      Just (VMFailure _) -> throwM $ SetUpCallFailed $ showTraceTree env.dapp vm4
       _ -> pure vm4
 
   where
diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index 3ed15922e..24189e7b0 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -38,8 +38,8 @@ panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
 checkAssertions :: [Word256] -> Postcondition
 checkAssertions _ _ vmres =
   case vmres of
-    Failure _ _ (UnrecognizedOpcode 0xfe) -> PBool False
-    Failure _ _ (Revert msg) -> case msg of
+    Failure _ _ _ -> PBool False
+    {-Failure _ _ (Revert msg) -> case msg of
       ConcreteBuf b ->
         -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
         let assertFail = (selector "Error(string)" `BS.isPrefixOf` b) &&
@@ -47,6 +47,7 @@ checkAssertions _ _ vmres =
         in if assertFail || b == panicMsg 0x01 then PBool False
         else PBool True
       _ -> error "Non-concrete revert message in assertion check"
+    -}
     _ -> PBool True
   where
     txtOffset = 4+32+32 -- selector + offset + length
@@ -161,7 +162,7 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   let
     vm' = vmReset & execState (loadContract (LitAddr dst))
                   & #tx % #isCreate .~ False
-                  & #state % #callvalue .~ TxValue
+                  & #state % #callvalue .~ (Lit 0) --TxValue
                   & #state % #caller .~ SymAddr "caller"
                   & #state % #calldata .~ cd
 
@@ -175,5 +176,5 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1]) Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
   let warnData = Just $ WarningData contract sources vm'
-  --liftIO $ mapM_ TIO.putStrLn partials
+  liftIO $ mapM_ (putStrLn . show) partials
   return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) partials)
diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs
index 6a4d214e3..a394ef050 100644
--- a/lib/Echidna/SymExec/Verification.hs
+++ b/lib/Echidna/SymExec/Verification.hs
@@ -56,6 +56,7 @@ verifyMethod method contract vm = do
     askSmtIters = conf.campaignConf.symExecAskSMTIters
     rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock))
     defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
+    --testMode = conf.campaignConf.testMode
 
   threadIdChan <- liftIO newEmptyMVar
   doneChan <- liftIO newEmptyMVar
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index 4d781a88c..c5425ad34 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -58,7 +58,7 @@ validateTestMode :: String -> TestMode
 validateTestMode s = case s of
   "property"     -> s
   "assertion"    -> s
-  "dapptest"     -> s
+  "foundry"     -> s
   "exploration"  -> s
   "overflow"     -> s
   "optimization" -> s
@@ -77,7 +77,7 @@ isPropertyMode "property" = True
 isPropertyMode _          = False
 
 isDapptestMode :: TestMode -> Bool
-isDapptestMode "dapptest"  = True
+isDapptestMode "foundry"  = True
 isDapptestMode _           = False
 
 createTests
@@ -99,7 +99,7 @@ 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" ->
+  "foundry" ->
     map (\s -> createTest (AssertionTest True s r))
         (filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ss)
   _ -> error validateTestModeError
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."
 

From e0dee282f9b78e6e8db3956c24e15d30d352adca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Mon, 26 Jan 2026 10:24:35 -0300
Subject: [PATCH 06/17] Update hevm to
 `542986dea3bec4f5898731ff48877a7a21811bf4`

---
 flake.nix                   |  4 ++--
 lib/Echidna/ABI.hs          | 10 +++++-----
 lib/Echidna/Orphans/JSON.hs |  7 +++++++
 lib/Echidna/Types/Tx.hs     |  6 +++++-
 stack.yaml                  |  2 +-
 5 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/flake.nix b/flake.nix
index c227e9320..ca865518c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -62,8 +62,8 @@
           (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "argotorg";
             repo = "hevm";
-            rev = "release/0.57.0";
-            sha256 = "sha256-Fn/u6u5euZ+khabqdOw7N29le29XCnxbOdSZOit+XXk=";
+            rev = "542986dea3bec4f5898731ff48877a7a21811bf4";
+            sha256 = "sha256-r17qrOEwUEoi6j45THYvk36LhrtVwhoHKI4kXcRDBYQ=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck
diff --git a/lib/Echidna/ABI.hs b/lib/Echidna/ABI.hs
index 4f8fe9217..cc0e9a6e4 100644
--- a/lib/Echidna/ABI.hs
+++ b/lib/Echidna/ABI.hs
@@ -77,7 +77,7 @@ ppAbiValue labels = \case
   AbiArrayDynamic _ v -> "[" <> commaSeparated v <> "]"
   AbiArray _ _ v      -> "[" <> commaSeparated v <> "]"
   AbiTuple v          -> "(" <> commaSeparated v <> ")"
-  AbiFunction v       -> show v
+  AbiFunction a sel   -> show a <> ":" <> show sel
   where
     commaSeparated v = intercalate ", " $ ppAbiValue labels <$> toList v
 
@@ -289,7 +289,7 @@ shrinkAbiValue = \case
     \case 0 -> AbiArrayDynamic t <$> traverse shrinkAbiValue l
           _ -> AbiArrayDynamic t <$> shrinkV l
   AbiTuple v          -> AbiTuple <$> traverse shrinkAbiValue' v
-  AbiFunction v       -> pure $ AbiFunction v
+  AbiFunction a sel   -> pure $ AbiFunction a sel
   where shrinkAbiValue' x = liftM3 bool (pure x) (shrinkAbiValue x) getRandom
 
 -- | Given a 'SolCall', generate a random \"smaller\" (simpler) call.
@@ -344,7 +344,7 @@ mutateAbiValue = \case
 
   AbiArrayDynamic t l -> AbiArrayDynamic t <$> mutateLL Nothing mempty l
   AbiTuple v -> AbiTuple <$> traverse mutateAbiValue v
-  AbiFunction v -> pure $ AbiFunction v
+  AbiFunction a sel -> pure $ AbiFunction a sel
 
 -- | Given a 'SolCall', generate a random \"similar\" call with the same 'SolSignature'.
 -- Note that this function will mutate a *single* argument (if any)
@@ -416,8 +416,8 @@ genAbiValueM' genDict funcName depth t =
                                  >>= flip V.replicateM (genAbiValueM' genDict funcName (depth + 1) t')
         AbiArrayType n t'      -> AbiArray n t' <$> V.replicateM n (genAbiValueM' genDict funcName (depth + 1) t')
         AbiTupleType v        -> AbiTuple <$> traverse (genAbiValueM' genDict funcName (depth + 1)) v
-        AbiFunctionType       -> liftM2 (\n -> AbiString . BS.pack . take n)
-                                        (getRandomR (1, 32)) getRandoms
+        AbiFunctionType       -> AbiFunction <$> rElem (NE.fromList pregenAdds)
+                                             <*> (FunctionSelector <$> getRandom)
   in genWithDict genDict genDict.constants go t
 
 -- | Given a 'SolSignature', generate a random 'SolCall' with that signature,
diff --git a/lib/Echidna/Orphans/JSON.hs b/lib/Echidna/Orphans/JSON.hs
index 9dd60c790..4016938ac 100644
--- a/lib/Echidna/Orphans/JSON.hs
+++ b/lib/Echidna/Orphans/JSON.hs
@@ -15,6 +15,7 @@ import Prelude hiding (Word, fail)
 import Text.Read (readMaybe)
 
 import EVM.ABI (AbiValue, AbiType)
+import EVM.Types (FunctionSelector)
 
 readT :: Read a => Text -> Maybe a
 readT = readMaybe . unpack
@@ -37,5 +38,11 @@ instance ToJSON ByteString where
 instance FromJSON ByteString where
   parseJSON = withText "ByteString" $ maybe (fail "could not parse ByteString") pure . readT
 
+instance ToJSON FunctionSelector where
+  toJSON = toJSON . show
+
+instance FromJSON FunctionSelector where
+  parseJSON = withText "FunctionSelector" $ maybe (fail "could not parse FunctionSelector") pure . readT
+
 $(deriveJSON defaultOptions ''AbiType)
 $(deriveJSON defaultOptions ''AbiValue)
diff --git a/lib/Echidna/Types/Tx.hs b/lib/Echidna/Types/Tx.hs
index 105b4946d..e62d140df 100644
--- a/lib/Echidna/Types/Tx.hs
+++ b/lib/Echidna/Types/Tx.hs
@@ -7,7 +7,7 @@
 module Echidna.Types.Tx where
 
 import Control.Applicative ((<|>))
-import Control.DeepSeq (NFData)
+import Control.DeepSeq (NFData(..))
 import Data.Aeson (FromJSON, ToJSON, parseJSON, toJSON, object, withObject, (.=), (.:))
 import Data.Aeson.TH (deriveJSON, defaultOptions)
 import Data.Aeson.Types (Parser)
@@ -76,6 +76,8 @@ deriving instance Hashable AbiValue
 deriving instance Hashable AbiType
 deriving anyclass instance Hashable Addr
 deriving anyclass instance Hashable W256
+instance Hashable FunctionSelector where
+  hashWithSalt s = hashWithSalt s . (.unFunctionSelector)
 
 deriving instance NFData Tx
 deriving instance NFData TxCall
@@ -88,6 +90,8 @@ deriving instance NFData Word160
 deriving instance NFData AbiType
 deriving anyclass instance NFData Addr
 deriving anyclass instance NFData W256
+instance NFData FunctionSelector where
+  rnf (FunctionSelector w) = rnf w
 
 instance ToJSON Tx where
   toJSON Tx{..} = object
diff --git a/stack.yaml b/stack.yaml
index 0059055f2..40229c5de 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: https://github.com/argotorg/hevm.git
-  commit: 5ec225475d5ba9cda24c5fb303acb76c88412553
+  commit: 542986dea3bec4f5898731ff48877a7a21811bf4
 
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162

From e34cff309e21583ec701ad7c1f192d5abb1acb4b Mon Sep 17 00:00:00 2001
From: Radu Bahmata <92028479+BowTiedRadone@users.noreply.github.com>
Date: Mon, 26 Jan 2026 15:53:17 +0200
Subject: [PATCH 07/17] Fix bugs in Foundry test generation (#1516)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Fix fallback function bug in Foundry test generation

* Fix null byte in argument bug in Foundry test generation

* Remove unnecessary config file

* Remove unused/redundant imports

* Disable Slither in Foundry test gen tests

* Conditionally run forge-std tests based on the solc version

* Reduce unnecessary test grouping and improve failed assertion messages

---------

Co-authored-by: Emilio López <2642849+elopez@users.noreply.github.com>
---
 lib/Echidna/Output/Foundry.hs                 |   5 +-
 package.yaml                                  |   1 +
 src/test/Tests/FoundryTestGen.hs              | 403 +++++++++---------
 tests/solidity/foundry/FallbackTest.sol       |  14 +
 tests/solidity/foundry/FoundryAsserts.yaml    |   1 +
 .../foundry/FoundryAssertsSymbolic.yaml       |   1 +
 tests/solidity/foundry/NullByteTest.sol       |   9 +
 tests/solidity/foundry/StatelessBug.yaml      |   1 +
 8 files changed, 241 insertions(+), 194 deletions(-)
 create mode 100644 tests/solidity/foundry/FallbackTest.sol
 create mode 100644 tests/solidity/foundry/NullByteTest.sol

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/package.yaml b/package.yaml
index 29a6a6431..4f19e71b3 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/test/Tests/FoundryTestGen.hs b/src/test/Tests/FoundryTestGen.hs
index d88416ff2..b26f97c8e 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -4,220 +4,172 @@ import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (testCase, assertFailure)
 
 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 (testContract, testContract', solved)
+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))
+import Test.Tasty.HUnit (assertBool)
 
 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)"
-      [ testGroup "assertTrue"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertTrueTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_true")
-              ]
+      [ testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertTrueTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertTrue should be detected concrete", solved "test_assert_true")
           ]
-      , testGroup "assertFalse"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertFalseTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_false")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertFalseTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertFalse should be detected concrete", solved "test_assert_false")
           ]
-      , testGroup "assertEq"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertEqTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_eq")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertEqTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertEq should be detected concrete", solved "test_assert_eq")
           ]
-      , testGroup "assertNotEq"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertNotEqTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_not_eq")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertNotEqTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertNotEq should be detected concrete", solved "test_assert_not_eq")
           ]
-      , testGroup "assertEqDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertEqDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_eq_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertEqDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertEqDecimal should be detected concrete", solved "test_assert_eq_decimal")
           ]
-      , testGroup "assertNotEqDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertNotEqDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_not_eq_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertNotEqDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertNotEqDecimal should be detected concrete", solved "test_assert_not_eq_decimal")
           ]
-      , testGroup "assertLt"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertLtTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_lt")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertLtTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLt should be detected concrete", solved "test_assert_lt")
           ]
-      , testGroup "assertGt"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertGtTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_gt")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertGtTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGt should be detected concrete", solved "test_assert_gt")
           ]
-      , testGroup "assertLtDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertLtDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_lt_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertLtDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLtDecimal should be detected concrete", solved "test_assert_lt_decimal")
           ]
-      , testGroup "assertGtDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertGtDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_gt_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertGtDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGtDecimal should be detected concrete", solved "test_assert_gt_decimal")
           ]
-      , testGroup "assertLe"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertLeTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_le")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertLeTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLe should be detected concrete", solved "test_assert_le")
           ]
-      , testGroup "assertGe"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertGeTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_ge")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertGeTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGe should be detected concrete", solved "test_assert_ge")
           ]
-      , testGroup "assertLeDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertLeDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_le_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertLeDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertLeDecimal should be detected concrete", solved "test_assert_le_decimal")
           ]
-      , testGroup "assertGeDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertGeDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_ge_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertGeDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertGeDecimal should be detected concrete", solved "test_assert_ge_decimal")
           ]
-      , testGroup "assertApproxEqAbs"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertApproxEqAbsTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_approx_eq_abs")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqAbsTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqAbs should be detected concrete", solved "test_assert_approx_eq_abs")
           ]
-      , testGroup "assertApproxEqAbsDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertApproxEqAbsDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_approx_eq_abs_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqAbsDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqAbsDecimal should be detected concrete", solved "test_assert_approx_eq_abs_decimal")
           ]
-      , testGroup "assertApproxEqRel"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertApproxEqRelTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_approx_eq_rel")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqRelTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqRel should be detected concrete", solved "test_assert_approx_eq_rel")
           ]
-      , testGroup "assertApproxEqRelDecimal"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertApproxEqRelDecimalTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected", solved "test_assert_approx_eq_rel_decimal")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertApproxEqRelDecimalTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("assertApproxEqRelDecimal should be detected concrete", solved "test_assert_approx_eq_rel_decimal")
           ]
-      , testGroup "stateless bug"
-          [ testContract "foundry/StatelessBug.sol" (Just "foundry/StatelessBug.yaml")
-              [ ("should be detected", solved "checkValue")
-              ]
+      , testContract "foundry/StatelessBug.sol" (Just "foundry/StatelessBug.yaml")
+          [ ("stateless bug should be detected concrete", solved "checkValue")
           ]
-      , testGroup "revert"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "RevertTest") Nothing (Just "foundry/FoundryAsserts.yaml")
-              True FuzzWorker
-              [ ("should be detected as failure", solved "test_revert_is_failure")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "RevertTest") (Just "foundry/FoundryAsserts.yaml")
+          FuzzWorker
+          [ ("revert should be detected as failure concrete", solved "test_revert_is_failure")
           ]
       ]
   , testGroup "Symbolic execution (SMT solving)"
-      [ testGroup "assertTrue"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertTrueTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_true")
-              ]
+      [ testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertTrueTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertTrue should be detected symbolic", solved "test_assert_true")
           ]
-      , testGroup "assertFalse"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertFalseTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_false")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertFalseTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertFalse should be detected symbolic", solved "test_assert_false")
           ]
-      , testGroup "assertEq"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertEqTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_eq")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertEqTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertEq should be detected symbolic", solved "test_assert_eq")
           ]
-      , testGroup "assertNotEq"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertNotEqTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_not_eq")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertNotEqTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertNotEq should be detected symbolic", solved "test_assert_not_eq")
           ]
-      , testGroup "assertLt"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertLtTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_lt")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertLtTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertLt should be detected symbolic", solved "test_assert_lt")
           ]
-      , testGroup "assertGt"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertGtTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_gt")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertGtTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertGt should be detected symbolic", solved "test_assert_gt")
           ]
-      , testGroup "assertLe"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertLeTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_le")
-              ]
+      , testForgeStd "foundry/FoundryAsserts.sol"
+          (Just "AssertLeTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
+          SymbolicWorker
+          [ ("assertLe should be detected symbolic", solved "test_assert_le")
           ]
-      , testGroup "assertGe"
-          [ testContract' "foundry/FoundryAsserts.sol"
-              (Just "AssertGeTest") Nothing (Just "foundry/FoundryAssertsSymbolic.yaml")
-              True SymbolicWorker
-              [ ("should be detected", solved "test_assert_ge")
-              ]
+      , testForgeStd "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
@@ -231,17 +183,41 @@ foundryTestGenTests = testGroup "Foundry test generation"
   ]
 
 -- | 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 ->
       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 ())
 
@@ -250,19 +226,17 @@ testForgeCompilation = do
       if code /= ExitSuccess
         then assertFailure $ "forge init failed: " ++ err
         else do
-          copyFile "foundry/FoundryTestTarget.sol" (tmpDir ++ "/src/FoundryTestTarget.sol")
+          copyFile contractPath (tmpDir ++ "/src/" ++ contractFile)
 
-          -- 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
+          -- 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\";"
+              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] ""
 
@@ -272,21 +246,6 @@ testForgeCompilation = do
             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
@@ -305,3 +264,61 @@ testBytes1Encoding = do
   if "hex\"92\"" `isInfixOf` generated
     then pure ()
     else assertFailure $ "bytes1 not correctly encoded: " ++ generated
+
+-- | Wrapper for testContract' that skips if solc < 0.8.13
+testForgeStd :: FilePath -> Maybe String -> Maybe FilePath -> WorkerType -> [(String, (Env, WorkerState) -> IO Bool)] -> TestTree
+testForgeStd fp contract config workerType checks =
+  if solcSupportsForgeStd
+    then testContract' fp (pack <$> contract) Nothing config True workerType checks
+    else testCase fp $ 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 $ if code == ExitSuccess
+               then maybe False (>= (0, 8, 13)) (parseSolcVersion out)
+               else False
+  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/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.yaml b/tests/solidity/foundry/FoundryAsserts.yaml
index 0e6e2696b..00421b26e 100644
--- a/tests/solidity/foundry/FoundryAsserts.yaml
+++ b/tests/solidity/foundry/FoundryAsserts.yaml
@@ -1,3 +1,4 @@
 testMode: dapptest
 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
index 58bc37a63..f4dc93815 100644
--- a/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
+++ b/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
@@ -5,3 +5,4 @@ symExec: true
 symExecSMTSolver: bitwuzla
 workers: 0
 seqLen: 1
+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.yaml b/tests/solidity/foundry/StatelessBug.yaml
index a21e7bb13..a47057f91 100644
--- a/tests/solidity/foundry/StatelessBug.yaml
+++ b/tests/solidity/foundry/StatelessBug.yaml
@@ -1,2 +1,3 @@
 testMode: assertion
 seed: 1234
+disableSlither: true

From b09b7b7514dc0db506465c3ac121bbfc2d1f71c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Tue, 27 Jan 2026 09:59:36 -0300
Subject: [PATCH 08/17] Update hevm to
 `41e6d1304411749ea8c816d131991663b5dca67a`

---
 flake.nix                           | 4 ++--
 lib/Echidna/SymExec/Exploration.hs  | 4 ++--
 lib/Echidna/SymExec/Verification.hs | 4 ++--
 stack.yaml                          | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/flake.nix b/flake.nix
index ca865518c..d82b516d6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -62,8 +62,8 @@
           (pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "argotorg";
             repo = "hevm";
-            rev = "542986dea3bec4f5898731ff48877a7a21811bf4";
-            sha256 = "sha256-r17qrOEwUEoi6j45THYvk36LhrtVwhoHKI4kXcRDBYQ=";
+            rev = "41e6d1304411749ea8c816d131991663b5dca67a";
+            sha256 = "sha256-JF4IyQ3OvfrIqybtCvCpz6nw6kgo39LLJSxOjXsw3/c=";
           }) { secp256k1 = pkgs.secp256k1; })
           ([
             pkgs.haskell.lib.compose.dontCheck
diff --git a/lib/Echidna/SymExec/Exploration.hs b/lib/Echidna/SymExec/Exploration.hs
index 7e66c980b..fd4b2907b 100644
--- a/lib/Echidna/SymExec/Exploration.hs
+++ b/lib/Echidna/SymExec/Exploration.hs
@@ -19,7 +19,7 @@ import EVM.Dapp (DappInfo(..))
 import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
 import EVM.Fetch (RpcInfo(..))
 import EVM.Solidity (SolcContract(..), Method(..))
-import EVM.Solvers (withSolvers)
+import EVM.Solvers (defMemLimit, withSolvers)
 import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..))
 import EVM.Types (VMType(..))
 import qualified EVM.Types (VM(..))
@@ -103,7 +103,7 @@ exploreContract contract method vm = do
   let runtimeEnv = defaultEnv { config = hevmConfig }
   session <- asks (.fetchSession)
   pushWorkerEvent $ SymExecLog ("Exploring " <> (show method.name))
-  liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeoutSMT $ \solvers -> do
+  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.
       -- In some cases, this methods list will have only one method, but in other cases, it will have several methods.
diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs
index 6a4d214e3..7a3e80ed5 100644
--- a/lib/Echidna/SymExec/Verification.hs
+++ b/lib/Echidna/SymExec/Verification.hs
@@ -17,7 +17,7 @@ import EVM.Dapp (DappInfo(..))
 import EVM.Effects (defaultEnv, defaultConfig, Config(..), Env(..))
 import EVM.Fetch (RpcInfo(..))
 import EVM.Solidity (SolcContract(..), Method(..))
-import EVM.Solvers (withSolvers)
+import EVM.Solvers (defMemLimit, withSolvers)
 import EVM.SymExec (IterConfig(..), LoopHeuristic (..), VeriOpts(..))
 import EVM.Types (VMType(..))
 import qualified EVM.Types (VM(..))
@@ -68,7 +68,7 @@ verifyMethod method contract vm = do
   session <- asks (.fetchSession)
   pushWorkerEvent $ SymExecLog ("Verifying " <> (show method.name))
 
-  liftIO $ flip runReaderT runtimeEnv $ withSolvers conf.campaignConf.symExecSMTSolver (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeoutSMT $ \solvers -> do
+  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) <- exploreMethod method contract dappInfo.sources vm defaultSender conf veriOpts solvers rpcInfo session
       liftIO $ putMVar resultChan (res, partials)
diff --git a/stack.yaml b/stack.yaml
index 40229c5de..035015722 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: https://github.com/argotorg/hevm.git
-  commit: 542986dea3bec4f5898731ff48877a7a21811bf4
+  commit: 41e6d1304411749ea8c816d131991663b5dca67a
 
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162

From 950bf92eca213050991d999aeed0bea0cf397802 Mon Sep 17 00:00:00 2001
From: Radu Bahmata <92028479+BowTiedRadone@users.noreply.github.com>
Date: Wed, 28 Jan 2026 09:26:34 +0200
Subject: [PATCH 09/17] Fix linter and build errors (#1521)

---
 lib/Echidna/SymExec/Common.hs    | 11 ++++-------
 src/test/Tests/FoundryTestGen.hs |  7 ++-----
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index 24189e7b0..5ef6f0929 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -5,7 +5,6 @@ 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.Function ((&))
 import Data.Map qualified as Map
@@ -24,7 +23,7 @@ import EVM.Format (formatPartialDetailed)
 import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData(..))
 import EVM.Solvers (SolverGroup)
 import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
-import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed, EvmError(..))
+import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
 import qualified EVM.Types (VM(..))
 
 import Echidna.Types (fromEVM)
@@ -38,7 +37,7 @@ panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
 checkAssertions :: [Word256] -> Postcondition
 checkAssertions _ _ vmres =
   case vmres of
-    Failure _ _ _ -> PBool False
+    Failure {} -> PBool False
     {-Failure _ _ (Revert msg) -> case msg of
       ConcreteBuf b ->
         -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
@@ -49,8 +48,6 @@ checkAssertions _ _ vmres =
       _ -> error "Non-concrete revert message in assertion check"
     -}
     _ -> PBool True
-  where
-    txtOffset = 4+32+32 -- selector + offset + length
 
 type PartialsLogs = [T.Text]
 
@@ -162,7 +159,7 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   let
     vm' = vmReset & execState (loadContract (LitAddr dst))
                   & #tx % #isCreate .~ False
-                  & #state % #callvalue .~ (Lit 0) --TxValue
+                  & #state % #callvalue .~ Lit 0 --TxValue
                   & #state % #caller .~ SymAddr "caller"
                   & #state % #calldata .~ cd
 
@@ -176,5 +173,5 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1]) Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
   let warnData = Just $ WarningData contract sources vm'
-  liftIO $ mapM_ (putStrLn . show) partials
+  liftIO $ mapM_ print partials
   return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) partials)
diff --git a/src/test/Tests/FoundryTestGen.hs b/src/test/Tests/FoundryTestGen.hs
index b26f97c8e..0a5437f08 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -1,7 +1,7 @@
 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.ByteString qualified as BS
@@ -22,7 +22,6 @@ 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))
-import Test.Tasty.HUnit (assertBool)
 
 foundryTestGenTests :: TestTree
 foundryTestGenTests = testGroup "Foundry test generation"
@@ -282,9 +281,7 @@ solcSupportsForgeStd = unsafePerformIO $ do
     Nothing -> pure False
     Just _ -> do
       (code, out, _) <- readProcessWithExitCode "solc" ["--version"] ""
-      pure $ if code == ExitSuccess
-               then maybe False (>= (0, 8, 13)) (parseSolcVersion out)
-               else False
+      pure $ code == ExitSuccess && maybe False (>= (0, 8, 13)) (parseSolcVersion out)
   where
     parseSolcVersion :: String -> Maybe (Int, Int, Int)
     parseSolcVersion output =

From d9908341e653110bc00df301923accafde5fdac8 Mon Sep 17 00:00:00 2001
From: gustavo-grieco <gustavo.grieco+github@gmail.com>
Date: Wed, 28 Jan 2026 09:14:35 +0100
Subject: [PATCH 10/17] improve foundry stateful invariant testing

---
 lib/Echidna.hs          |  3 ++-
 lib/Echidna/Solidity.hs |  6 ++++--
 lib/Echidna/Test.hs     | 13 +++++++++----
 3 files changed, 15 insertions(+), 7 deletions(-)

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/Solidity.hs b/lib/Echidna/Solidity.hs
index 8664bd34d..ffbcd4d16 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -149,7 +149,7 @@ filterMethods contractName (Blacklist ig) ms =
 -- | Filter methods with arguments, used for dapptest mode
 filterMethodsWithArgs :: NonEmpty SolSignature -> NonEmpty SolSignature
 filterMethodsWithArgs ms =
-  case NE.filter (\(n, xs) -> T.isPrefixOf "test" n && (T.isPrefixOf "invariant_" n || not (null xs))) ms of
+  case NE.filter (\(n, xs) -> T.isPrefixOf "test" n || (T.isPrefixOf "invariant_" n || not (null xs))) ms of
     [] -> error "No dapptest tests found"
     fs -> NE.fromList fs
 
@@ -285,9 +285,10 @@ 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)
@@ -310,6 +311,7 @@ mkTests solConf mainContract = do
   pure $ createTests solConf.testMode
                      solConf.testDestruction
                      testNames
+                     campaignConf.seqLen
                      solConf.contractAddr
                      neFuns
 
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index c5425ad34..452f93a25 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -84,10 +84,11 @@ createTests
   :: TestMode
   -> Bool
   -> [Text]
+  -> Int
   -> Addr
   -> [SolSignature]
   -> [EchidnaTest]
-createTests m td ts r ss = case m of
+createTests m td ts len r ss = case m of
   "exploration" ->
     [createTest Exploration]
   "overflow" ->
@@ -100,8 +101,12 @@ createTests m td ts r ss = case m of
     map (\s -> createTest (AssertionTest False s r))
         (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)]
   "foundry" ->
-    map (\s -> createTest (AssertionTest True s r))
-        (filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ss)
+    if (len == 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
@@ -244,7 +249,7 @@ checkDapptestAssertion vm sig addr = do
                     (forceBuf vm.state.calldata)
     isAssertionFailure = case vm.result of
       Just (VMFailure (Revert (ConcreteBuf bs))) ->
-        not $ BS.isSuffixOf assumeMagicReturnCode bs
+        (T.isPrefixOf "invariant_" $ fst sig) && (not $ BS.isSuffixOf assumeMagicReturnCode bs)
       Just (VMFailure _) -> True
       _ -> False
     isCorrectAddr = LitAddr addr == vm.state.codeContract

From 90752af9b1e0c8a8a09bafc48d021bf089c3ba0e Mon Sep 17 00:00:00 2001
From: gustavo-grieco <gustavo.grieco+github@gmail.com>
Date: Wed, 28 Jan 2026 14:19:33 +0100
Subject: [PATCH 11/17] fix

---
 lib/Echidna/SymExec/Common.hs | 2 +-
 lib/Echidna/Test.hs           | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index 5ef6f0929..447a59029 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -173,5 +173,5 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   (models, partials) <- verifyInputsWithHandler solvers veriOpts fetcher vm'' (checkAssertions [0x1]) Nothing
   let results = filter (\(r, _) -> not (isQed r)) models & map fst
   let warnData = Just $ WarningData contract sources vm'
-  liftIO $ mapM_ print partials
+  --liftIO $ mapM_ print partials
   return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) partials)
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index 452f93a25..b92ccdeb8 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -249,6 +249,7 @@ checkDapptestAssertion vm sig addr = do
                     (forceBuf vm.state.calldata)
     isAssertionFailure = case vm.result of
       Just (VMFailure (Revert (ConcreteBuf bs))) ->
+        (T.isPrefixOf "test" $ fst sig) && (not $ BS.isSuffixOf assumeMagicReturnCode bs) ||
         (T.isPrefixOf "invariant_" $ fst sig) && (not $ BS.isSuffixOf assumeMagicReturnCode bs)
       Just (VMFailure _) -> True
       _ -> False

From c3685e75e18caf96b01026e388a15bb43780f714 Mon Sep 17 00:00:00 2001
From: Radu Bahmata <92028479+BowTiedRadone@users.noreply.github.com>
Date: Sat, 31 Jan 2026 09:06:11 +0200
Subject: [PATCH 12/17] Fix foundry test generation linter hints and tests
 (#1522)

---
 lib/Echidna/SourceAnalysis/Slither.hs         |  17 +--
 lib/Echidna/Test.hs                           |  10 +-
 src/test/Common.hs                            |  17 ++-
 src/test/Tests/FoundryTestGen.hs              | 105 ++++++++++++------
 tests/solidity/dapptest/config.yaml           |   2 +-
 tests/solidity/foundry/FoundryAsserts.sol     |  14 +++
 tests/solidity/foundry/FoundryAsserts.yaml    |   2 +-
 .../foundry/FoundryAssertsSymbolic.yaml       |   2 +-
 tests/solidity/foundry/FoundryInvariant.yaml  |   4 +
 9 files changed, 120 insertions(+), 53 deletions(-)
 create mode 100644 tests/solidity/foundry/FoundryInvariant.yaml

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/Test.hs b/lib/Echidna/Test.hs
index b92ccdeb8..55c8aef02 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -52,7 +52,7 @@ 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
@@ -101,10 +101,10 @@ createTests m td ts len r ss = case m of
     map (\s -> createTest (AssertionTest False s r))
         (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)]
   "foundry" ->
-    if (len == 1) then
+    if len == 1 then
       map (\s -> createTest (AssertionTest True s r))
         (filter (\(n, xs) -> T.isPrefixOf "test" n && not (null xs)) ss)
-    else 
+    else
       map (\s -> createTest (AssertionTest True s r))
           (filter (\(n, xs) -> T.isPrefixOf "invariant_" n || not (null xs)) ss)
   _ -> error validateTestModeError
@@ -249,8 +249,8 @@ checkDapptestAssertion vm sig addr = do
                     (forceBuf vm.state.calldata)
     isAssertionFailure = case vm.result of
       Just (VMFailure (Revert (ConcreteBuf bs))) ->
-        (T.isPrefixOf "test" $ fst sig) && (not $ BS.isSuffixOf assumeMagicReturnCode bs) ||
-        (T.isPrefixOf "invariant_" $ fst sig) && (not $ BS.isSuffixOf assumeMagicReturnCode bs)
+        T.isPrefixOf "test" (fst sig) && not (BS.isSuffixOf assumeMagicReturnCode bs) ||
+        T.isPrefixOf "invariant_" (fst sig) && not (BS.isSuffixOf assumeMagicReturnCode bs)
       Just (VMFailure _) -> True
       _ -> False
     isCorrectAddr = LitAddr addr == vm.state.codeContract
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/Tests/FoundryTestGen.hs b/src/test/Tests/FoundryTestGen.hs
index 0a5437f08..fa9334a09 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -14,7 +14,7 @@ import System.IO.Unsafe (unsafePerformIO)
 import System.Process (readProcessWithExitCode)
 import Text.Read (readMaybe)
 
-import Common (testContract, testContract', solved)
+import Common (solved, testContract, testContractNamed)
 import Echidna.Types.Config (Env)
 import Echidna.Types.Campaign (WorkerState)
 import EVM.ABI (AbiValue(..))
@@ -30,92 +30,110 @@ foundryTestGenTests = testGroup "Foundry test generation"
   , testCase "fallback function syntax" testFallbackSyntax
   , testCase "null bytes in arguments" testNullBytes
   , testGroup "Concrete execution (fuzzing)"
-      [ testForgeStd "foundry/FoundryAsserts.sol"
+      [ testForgeStd "solves assertTrue"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertTrueTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertTrue should be detected concrete", solved "test_assert_true")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertFalse"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertFalseTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertFalse should be detected concrete", solved "test_assert_false")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertEq"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertEqTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertEq should be detected concrete", solved "test_assert_eq")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertNotEq"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertNotEqTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertNotEq should be detected concrete", solved "test_assert_not_eq")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertEqDecimal"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertEqDecimalTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertEqDecimal should be detected concrete", solved "test_assert_eq_decimal")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , 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 "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertLt"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertLtTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertLt should be detected concrete", solved "test_assert_lt")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertGt"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertGtTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertGt should be detected concrete", solved "test_assert_gt")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertLtDecimal"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertLtDecimalTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertLtDecimal should be detected concrete", solved "test_assert_lt_decimal")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertGtDecimal"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertGtDecimalTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertGtDecimal should be detected concrete", solved "test_assert_gt_decimal")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertLe"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertLeTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertLe should be detected concrete", solved "test_assert_le")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertGe"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertGeTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertGe should be detected concrete", solved "test_assert_ge")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertLeDecimal"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertLeDecimalTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertLeDecimal should be detected concrete", solved "test_assert_le_decimal")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertGeDecimal"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertGeDecimalTest") (Just "foundry/FoundryAsserts.yaml")
           FuzzWorker
           [ ("assertGeDecimal should be detected concrete", solved "test_assert_ge_decimal")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , 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 "foundry/FoundryAsserts.sol"
+      , 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 "foundry/FoundryAsserts.sol"
+      , 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 "foundry/FoundryAsserts.sol"
+      , 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")
@@ -123,49 +141,64 @@ foundryTestGenTests = testGroup "Foundry test generation"
       , testContract "foundry/StatelessBug.sol" (Just "foundry/StatelessBug.yaml")
           [ ("stateless bug should be detected concrete", solved "checkValue")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , 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")
+          ]
       ]
   , testGroup "Symbolic execution (SMT solving)"
-      [ testForgeStd "foundry/FoundryAsserts.sol"
+      [ testForgeStd "solves assertTrue"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertTrueTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertTrue should be detected symbolic", solved "test_assert_true")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertFalse"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertFalseTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertFalse should be detected symbolic", solved "test_assert_false")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertEq"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertEqTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertEq should be detected symbolic", solved "test_assert_eq")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertNotEq"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertNotEqTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertNotEq should be detected symbolic", solved "test_assert_not_eq")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertLt"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertLtTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertLt should be detected symbolic", solved "test_assert_lt")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertGt"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertGtTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertGt should be detected symbolic", solved "test_assert_gt")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertLe"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertLeTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertLe should be detected symbolic", solved "test_assert_le")
           ]
-      , testForgeStd "foundry/FoundryAsserts.sol"
+      , testForgeStd "solves assertGe"
+          "foundry/FoundryAsserts.sol"
           (Just "AssertGeTest") (Just "foundry/FoundryAssertsSymbolic.yaml")
           SymbolicWorker
           [ ("assertGe should be detected symbolic", solved "test_assert_ge")
@@ -264,12 +297,12 @@ testBytes1Encoding = do
     then pure ()
     else assertFailure $ "bytes1 not correctly encoded: " ++ generated
 
--- | Wrapper for testContract' that skips if solc < 0.8.13
-testForgeStd :: FilePath -> Maybe String -> Maybe FilePath -> WorkerType -> [(String, (Env, WorkerState) -> IO Bool)] -> TestTree
-testForgeStd fp contract config workerType checks =
+-- | 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 testContract' fp (pack <$> contract) Nothing config True workerType checks
-    else testCase fp $ assertBool "skip (solc < 0.8.13, forge-std requires >= 0.8.13)" True
+    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.
@@ -286,7 +319,7 @@ solcSupportsForgeStd = unsafePerformIO $ do
     parseSolcVersion :: String -> Maybe (Int, Int, Int)
     parseSolcVersion output =
       case filter ("Version:" `isPrefixOf`) (lines output) of
-        (line:_) -> 
+        (line:_) ->
           let versionPart = dropWhile (/= ':') line
               version = takeWhile (/= '+') $ drop 2 versionPart
               parts = words version
@@ -294,12 +327,12 @@ solcSupportsForgeStd = unsafePerformIO $ do
                (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
diff --git a/tests/solidity/dapptest/config.yaml b/tests/solidity/dapptest/config.yaml
index 6ce1300dd..328392dea 100644
--- a/tests/solidity/dapptest/config.yaml
+++ b/tests/solidity/dapptest/config.yaml
@@ -1,4 +1,4 @@
-testMode: dapptest
+testMode: foundry
 testLimit: 5000
 shrinkLimit: 100
 seqLen: 1
diff --git a/tests/solidity/foundry/FoundryAsserts.sol b/tests/solidity/foundry/FoundryAsserts.sol
index 3b99cc435..1da4455ce 100644
--- a/tests/solidity/foundry/FoundryAsserts.sol
+++ b/tests/solidity/foundry/FoundryAsserts.sol
@@ -136,6 +136,20 @@ contract AssertApproxEqRelDecimalTest is Test {
     }
 }
 
+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 {
diff --git a/tests/solidity/foundry/FoundryAsserts.yaml b/tests/solidity/foundry/FoundryAsserts.yaml
index 00421b26e..e1c90df7c 100644
--- a/tests/solidity/foundry/FoundryAsserts.yaml
+++ b/tests/solidity/foundry/FoundryAsserts.yaml
@@ -1,4 +1,4 @@
-testMode: dapptest
+testMode: foundry
 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
index f4dc93815..ea114f0f2 100644
--- a/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
+++ b/tests/solidity/foundry/FoundryAssertsSymbolic.yaml
@@ -1,4 +1,4 @@
-testMode: dapptest
+testMode: foundry
 seed: 1234
 cryticArgs: ["--solc-remaps", "forge-std/=foundry/forge-std/src/"]
 symExec: 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

From 44b19daa62bf4934ff4569a2bd2e7df445ac1670 Mon Sep 17 00:00:00 2001
From: Radu Bahmata <92028479+BowTiedRadone@users.noreply.github.com>
Date: Mon, 2 Mar 2026 19:26:40 +0200
Subject: [PATCH 13/17] Foundry updates (#1525)

* Rename dapptest to foundry and support foundry assertX in assertion mode

* Rename basic foundry test contracts dir to `foundry-basic`

* Add testing modes to `README`
---
 README.md                                     | 15 ++++++++--
 lib/Echidna/Solidity.hs                       | 14 ++++-----
 lib/Echidna/Test.hs                           | 12 ++++----
 src/Main.hs                                   |  2 +-
 src/test/Spec.hs                              |  4 +--
 src/test/Tests/{Dapptest.hs => Foundry.hs}    | 12 ++++----
 src/test/Tests/FoundryTestGen.hs              | 20 +++++++++++++
 .../{dapptest => foundry-basic}/basic.sol     |  0
 .../{dapptest => foundry-basic}/config.yaml   |  0
 .../foundry/FoundryAssertsAssertionMode.sol   | 29 +++++++++++++++++++
 .../foundry/FoundryAssertsAssertionMode.yaml  |  4 +++
 11 files changed, 88 insertions(+), 24 deletions(-)
 rename src/test/Tests/{Dapptest.hs => Foundry.hs} (71%)
 rename tests/solidity/{dapptest => foundry-basic}/basic.sol (100%)
 rename tests/solidity/{dapptest => foundry-basic}/config.yaml (100%)
 create mode 100644 tests/solidity/foundry/FoundryAssertsAssertionMode.sol
 create mode 100644 tests/solidity/foundry/FoundryAssertsAssertionMode.yaml

diff --git a/README.md b/README.md
index c8f10c177..d2b0973cb 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_opt_`-prefixed functions.
+* **`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/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index ffbcd4d16..782e1593f 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,11 @@ 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 with arguments, used for foundry mode
 filterMethodsWithArgs :: NonEmpty SolSignature -> NonEmpty SolSignature
 filterMethodsWithArgs ms =
   case NE.filter (\(n, xs) -> T.isPrefixOf "test" n || (T.isPrefixOf "invariant_" n || not (null xs))) ms of
-    [] -> error "No dapptest tests found"
+    [] -> error "No foundry tests found"
     fs -> NE.fromList fs
 
 abiOf :: Text -> SolcContract -> NonEmpty SolSignature
@@ -260,7 +260,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
@@ -277,7 +277,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
@@ -293,7 +293,7 @@ mkTests solConf campaignConf mainContract = do
     -- 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)
@@ -351,7 +351,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/Test.hs b/lib/Echidna/Test.hs
index 55c8aef02..d55c5325c 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -76,9 +76,9 @@ isPropertyMode :: TestMode -> Bool
 isPropertyMode "property" = True
 isPropertyMode _          = False
 
-isDapptestMode :: TestMode -> Bool
-isDapptestMode "foundry"  = True
-isDapptestMode _           = False
+isFoundryMode :: TestMode -> Bool
+isFoundryMode "foundry"  = True
+isFoundryMode _           = False
 
 createTests
   :: TestMode
@@ -148,7 +148,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
 
@@ -233,13 +233,13 @@ checkStatefulAssertion vm sig addr = do
 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
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/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 fa9334a09..73e279b50 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -212,6 +212,26 @@ foundryTestGenTests = testGroup "Foundry test generation"
       -- - 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.
diff --git a/tests/solidity/dapptest/basic.sol b/tests/solidity/foundry-basic/basic.sol
similarity index 100%
rename from tests/solidity/dapptest/basic.sol
rename to tests/solidity/foundry-basic/basic.sol
diff --git a/tests/solidity/dapptest/config.yaml b/tests/solidity/foundry-basic/config.yaml
similarity index 100%
rename from tests/solidity/dapptest/config.yaml
rename to tests/solidity/foundry-basic/config.yaml
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

From dee8b2fb38fd39a36e004d18e2bc60636f2bec4a Mon Sep 17 00:00:00 2001
From: gustavo-grieco <gustavo.grieco+github@gmail.com>
Date: Tue, 3 Mar 2026 09:57:04 +0100
Subject: [PATCH 14/17] fixes

---
 lib/Echidna/Campaign.hs             |  2 --
 lib/Echidna/SymExec/Common.hs       | 53 ++++++++++++++++++++---------
 lib/Echidna/SymExec/Verification.hs |  1 -
 lib/Echidna/Test.hs                 | 14 +++++---
 4 files changed, 46 insertions(+), 24 deletions(-)

diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index ec81bbe86..0543822f6 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -288,8 +288,6 @@ runSymWorker callback vm dict workerId _ name = do
     lift callback
 
     (symTxs, partials) <- liftIO $ takeMVar symTxsChan
-    liftIO $ print symTxs
-    liftIO $ print partials
     let txs = extractTxs symTxs
     let errors = extractErrors symTxs
 
diff --git a/lib/Echidna/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index 447a59029..eb5bf7d0b 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -5,7 +5,9 @@ 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)
@@ -23,9 +25,10 @@ import EVM.Format (formatPartialDetailed)
 import EVM.Solidity (SolcContract(..), SourceCache(..), Method(..), WarningData(..))
 import EVM.Solvers (SolverGroup)
 import EVM.SymExec (mkCalldata, verifyInputsWithHandler, VeriOpts(..), subModel, defaultSymbolicValues, Postcondition)
-import EVM.Types (Addr, VMType(..), EType(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
+import EVM.Types (Addr, VMType(..), EType(..), EvmError(..), Expr(..), Block(..), W256, SMTCex(..), ProofResult(..), Prop(..), forceLit, isQed)
 import qualified EVM.Types (VM(..))
 
+import Echidna.Test (assumeMagicReturnCode, isFoundryMode)
 import Echidna.Types (fromEVM)
 import Echidna.Types.Config (EConfig(..))
 import Echidna.Types.Solidity (SolConf(..))
@@ -34,20 +37,36 @@ import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..), maxGasPerBlock)
 panicMsg :: Word256 -> ByteString
 panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
 
-checkAssertions :: [Word256] -> Postcondition
-checkAssertions _ _ vmres =
-  case vmres of
-    Failure {} -> PBool False
-    {-Failure _ _ (Revert msg) -> case msg of
-      ConcreteBuf b ->
+-- | 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 _ _ (Revert (ConcreteBuf bs))
+        | assumeMagicReturnCode `BS.isSuffixOf` bs -> 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` b) &&
-              ("assertion failed" `BS.isPrefixOf` BS.drop txtOffset b)
-        in if assertFail || b == panicMsg 0x01 then PBool False
-        else PBool True
-      _ -> error "Non-concrete revert message in assertion check"
-    -}
-    _ -> PBool True
+        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]
 
@@ -159,7 +178,8 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   let
     vm' = vmReset & execState (loadContract (LitAddr dst))
                   & #tx % #isCreate .~ False
-                  & #state % #callvalue .~ Lit 0 --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
 
@@ -170,7 +190,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_ print partials
diff --git a/lib/Echidna/SymExec/Verification.hs b/lib/Echidna/SymExec/Verification.hs
index 9d3e5f261..7a3e80ed5 100644
--- a/lib/Echidna/SymExec/Verification.hs
+++ b/lib/Echidna/SymExec/Verification.hs
@@ -56,7 +56,6 @@ verifyMethod method contract vm = do
     askSmtIters = conf.campaignConf.symExecAskSMTIters
     rpcInfo = RpcInfo (rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock))
     defaultSender = fromJust $ Set.lookupMin conf.solConf.sender <|> Just 0
-    --testMode = conf.campaignConf.testMode
 
   threadIdChan <- liftIO newEmptyMVar
   doneChan <- liftIO newEmptyMVar
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index d55c5325c..1838b6eec 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -58,7 +58,7 @@ validateTestMode :: String -> TestMode
 validateTestMode s = case s of
   "property"     -> s
   "assertion"    -> s
-  "foundry"     -> s
+  "foundry"      -> s
   "exploration"  -> s
   "overflow"     -> s
   "optimization" -> s
@@ -77,8 +77,8 @@ isPropertyMode "property" = True
 isPropertyMode _          = False
 
 isFoundryMode :: TestMode -> Bool
-isFoundryMode "foundry"  = True
-isFoundryMode _           = False
+isFoundryMode "foundry" = True
+isFoundryMode _          = False
 
 createTests
   :: TestMode
@@ -88,7 +88,7 @@ createTests
   -> Addr
   -> [SolSignature]
   -> [EchidnaTest]
-createTests m td ts len r ss = case m of
+createTests m td ts seqLen r ss = case m of
   "exploration" ->
     [createTest Exploration]
   "overflow" ->
@@ -100,8 +100,10 @@ createTests m td ts len r ss = case m of
   "assertion" ->
     map (\s -> createTest (AssertionTest False s r))
         (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)]
+  -- In foundry mode, seqLen distinguishes fuzz tests (seqLen == 1) from
+  -- invariant tests (seqLen > 1), which determines how functions are filtered.
   "foundry" ->
-    if len == 1 then
+    if seqLen == 1 then
       map (\s -> createTest (AssertionTest True s r))
         (filter (\(n, xs) -> T.isPrefixOf "test" n && not (null xs)) ss)
     else
@@ -230,6 +232,8 @@ checkStatefulAssertion vm sig addr = do
     isFailure = isCorrectTarget && (eventFailure || isAssertionFailure)
   pure (BoolValue (not isFailure), vm)
 
+-- | Magic return code used by hevm to signal a foundry vm.assume failure.
+-- See: https://github.com/ethereum/hevm/blob/main/src/EVM.hs (search for FOUNDRY::ASSUME)
 assumeMagicReturnCode :: BS.ByteString
 assumeMagicReturnCode = "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0"
 

From 21b8f54e1caa2f21e2bcd4e7a492c5312fd455cf Mon Sep 17 00:00:00 2001
From: gustavo-grieco <gustavo.grieco+github@gmail.com>
Date: Tue, 3 Mar 2026 10:02:40 +0100
Subject: [PATCH 15/17] fixes

---
 lib/Echidna/Solidity.hs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index 782e1593f..2e585d401 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -146,7 +146,15 @@ 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 foundry 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 "test" n || (T.isPrefixOf "invariant_" n || not (null xs))) ms of

From f11eacfbcfca959434cde2998e9f6ff4a134620d Mon Sep 17 00:00:00 2001
From: Radu Bahmata <92028479+BowTiedRadone@users.noreply.github.com>
Date: Wed, 4 Mar 2026 00:45:52 +0200
Subject: [PATCH 16/17] Add support for Foundry assume (#1528)

---
 lib/Echidna/Exec.hs                       |  1 +
 lib/Echidna/SymExec/Common.hs             | 12 +++++-------
 lib/Echidna/Test.hs                       | 12 ++++--------
 lib/Echidna/Types/Tx.hs                   |  2 ++
 src/test/Tests/FoundryTestGen.hs          |  8 +++++++-
 stack.yaml                                |  2 +-
 tests/solidity/foundry-basic/basic.sol    | 11 +++++++++--
 tests/solidity/foundry/FoundryAsserts.sol | 10 ++++++++++
 8 files changed, 39 insertions(+), 19 deletions(-)

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/SymExec/Common.hs b/lib/Echidna/SymExec/Common.hs
index eb5bf7d0b..cae5d8d17 100644
--- a/lib/Echidna/SymExec/Common.hs
+++ b/lib/Echidna/SymExec/Common.hs
@@ -22,13 +22,13 @@ 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(..), 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 (assumeMagicReturnCode, isFoundryMode)
+import Echidna.Test (isFoundryMode)
 import Echidna.Types (fromEVM)
 import Echidna.Types.Config (EConfig(..))
 import Echidna.Types.Solidity (SolConf(..))
@@ -45,8 +45,7 @@ checkAssertions :: [Word256] -> Bool -> Postcondition
 checkAssertions errs isFoundry _ vmres
   | isFoundry = case vmres of
       -- vm.assume failures should not be treated as test failures
-      Failure _ _ (Revert (ConcreteBuf bs))
-        | assumeMagicReturnCode `BS.isSuffixOf` bs -> PBool True
+      Failure _ _ AssumeCheatFailed -> PBool True
       -- All other failures are test failures in foundry mode
       Failure {} -> PBool False
       _ -> PBool True
@@ -168,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
@@ -193,6 +192,5 @@ exploreMethod method contract sources vm defaultSender conf veriOpts solvers rpc
   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_ print partials
-  return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender cd) results, map (formatPartialDetailed warnData . fst) 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 1838b6eec..be277953d 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -232,11 +232,6 @@ checkStatefulAssertion vm sig addr = do
     isFailure = isCorrectTarget && (eventFailure || isAssertionFailure)
   pure (BoolValue (not isFailure), vm)
 
--- | Magic return code used by hevm to signal a foundry vm.assume failure.
--- See: https://github.com/ethereum/hevm/blob/main/src/EVM.hs (search for FOUNDRY::ASSUME)
-assumeMagicReturnCode :: BS.ByteString
-assumeMagicReturnCode = "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0"
-
 checkFoundryAssertion
   :: (MonadReader Env m, MonadThrow m)
   => VM Concrete
@@ -252,9 +247,10 @@ checkFoundryAssertion 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))) ->
-        T.isPrefixOf "test" (fst sig) && not (BS.isSuffixOf assumeMagicReturnCode bs) ||
-        T.isPrefixOf "invariant_" (fst sig) && 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/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/src/test/Tests/FoundryTestGen.hs b/src/test/Tests/FoundryTestGen.hs
index 73e279b50..86017229c 100644
--- a/src/test/Tests/FoundryTestGen.hs
+++ b/src/test/Tests/FoundryTestGen.hs
@@ -14,7 +14,7 @@ import System.IO.Unsafe (unsafePerformIO)
 import System.Process (readProcessWithExitCode)
 import Text.Read (readMaybe)
 
-import Common (solved, testContract, testContractNamed)
+import Common (solved, passed, testContract, testContractNamed)
 import Echidna.Types.Config (Env)
 import Echidna.Types.Campaign (WorkerState)
 import EVM.ABI (AbiValue(..))
@@ -153,6 +153,12 @@ foundryTestGenTests = testGroup "Foundry test generation"
           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"
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/foundry-basic/basic.sol b/tests/solidity/foundry-basic/basic.sol
index 572c2efc0..612e6e362 100644
--- a/tests/solidity/foundry-basic/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/foundry/FoundryAsserts.sol b/tests/solidity/foundry/FoundryAsserts.sol
index 1da4455ce..14f752372 100644
--- a/tests/solidity/foundry/FoundryAsserts.sol
+++ b/tests/solidity/foundry/FoundryAsserts.sol
@@ -157,4 +157,14 @@ contract RevertTest is Test {
             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

From 1ef15b9c9b72b4dd333ee6428e3e64574d40c229 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20L=C3=B3pez?= <emilio.lopez@trailofbits.com>
Date: Tue, 3 Mar 2026 20:21:13 -0300
Subject: [PATCH 17/17] flake: sync hevm version with stack.yaml

---
 flake.nix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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