diff --git a/CHANGELOG.md b/CHANGELOG.md
index 26eaa328a..06cc26dc7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - More complete and precise array/mapping slot rewrite, along with a copySlice improvement
 - Use a let expression in copySlice to decrease expression size
 - The `--debug` flag now dumps the internal expressions as well
+- hevm now uses the forge-std library's way of detecting failures, i.e. through
+  reverting with a specific error code unless --assertion-type DSTest is passed
 
 ## Added
 - More POr and PAnd rules
@@ -41,6 +43,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   partial results instead of erroring out
 - Fix interpreter's MCOPY handling so that it doesn't error out on symbolic arguments
 - More desciptive errors in case of a cheatcode issue
+- Better and more pretty debug messages
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing
@@ -63,6 +66,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Respect --smt-timeout in equivalence checking
 - Fixed the handling of returndata with an abstract size during transaction finalization
 - Error handling for user-facing cli commands is much improved
+- Fixed call signature generation for test cases
 - Fixing prank so it doesn't override the sender address on lower call frames
 
 ## [0.53.0] - 2024-02-23
diff --git a/cli/cli.hs b/cli/cli.hs
index 6517e8386..3015cecb2 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -47,6 +47,9 @@ import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
 
+data AssertionType = DSTest | Forge
+  deriving (Eq, Show, Read, ParseField)
+
 -- This record defines the program's command-line options
 -- automatically via the `optparse-generic` package.
 data Command w
@@ -77,7 +80,8 @@ data Command w
 
   -- symbolic execution opts
       , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
       , arg           :: w ::: [String]           <?> "Values to encode"
@@ -147,11 +151,13 @@ data Command w
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       }
-  | Test -- Run DSTest unit tests
+  | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
+      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
@@ -674,6 +680,7 @@ unitTestOptions cmd solvers buildOutput = do
     , testParams = params
     , dapp = srcInfo
     , ffiAllowed = cmd.ffi
+    , checkFailBit = (fromMaybe Forge cmd.assertionType) == DSTest
     }
 parseInitialStorage :: InitialStorage -> BaseState
 parseInitialStorage Empty = EmptyBase
diff --git a/doc/src/exec.md b/doc/src/exec.md
index ea5db639f..f85d27145 100644
--- a/doc/src/exec.md
+++ b/doc/src/exec.md
@@ -38,13 +38,11 @@ Available options:
   --rpc TEXT               Fetch state from a remote node
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
+  --project-type PROJECTTYPE Foundry or CombinedJSON project
 ```
 
 Minimum required flags: either you must provide `--code` or you must both pass
-`--rpc` and `--address`. 
+`--rpc` and `--address`.
 
 If the execution returns an output, it will be written
 to stdout. Exit code indicates whether the execution was successful or
diff --git a/doc/src/getting-started.md b/doc/src/getting-started.md
index 25bbbcb7e..f057b72f9 100644
--- a/doc/src/getting-started.md
+++ b/doc/src/getting-started.md
@@ -28,9 +28,9 @@ be larger than or equal to 100. Let's see the contract and its associated check:
 
 ```solidity
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "foge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   mapping (address => uint) balances;
   function prove_add_value(address recv, uint amt) public {
     require(balances[recv] < 100);
@@ -65,9 +65,9 @@ $ chmod +x ./hevm-x86_64-linux
 $ forge init .
 $ cat <<EOF > src/contract.sol
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   mapping (address => uint) balances;
   function prove_add_value(address recv, uint amt) public {
     require(balances[recv] < 100);
diff --git a/doc/src/symbolic.md b/doc/src/symbolic.md
index ed9b74463..f88d6e8b6 100644
--- a/doc/src/symbolic.md
+++ b/doc/src/symbolic.md
@@ -41,9 +41,7 @@ Available options:
   --rpc TEXT               Fetch state from a remote node
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
+  --project-type PROJECTTYPE Foundry or CombinedJSON project
   --initial-storage INITIALSTORAGE
                            Starting state for storage: Empty, Abstract (default
                            Abstract)
diff --git a/doc/src/test.md b/doc/src/test.md
index 44f1b186e..6359b6eb1 100644
--- a/doc/src/test.md
+++ b/doc/src/test.md
@@ -13,9 +13,7 @@ Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
 Available options:
   -h,--help                Show this help text
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
+  --project-type PROJECTTYPE Foundry or CombinedJSON project
   --rpc TEXT               Fetch state from a remote node
   --number W256            Block: number
   --verbose INT            Append call trace: {1} failures {2} all
diff --git a/doc/src/when-to-use.md b/doc/src/when-to-use.md
index e40b4dc08..4b98a9dfb 100644
--- a/doc/src/when-to-use.md
+++ b/doc/src/when-to-use.md
@@ -26,9 +26,9 @@ bytecode, postconditions need to be explicit. Let's see an example:
 ```solidity
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   uint balance;
   function test_overflow(uint amt) public {
     unchecked {
@@ -50,9 +50,9 @@ towards them. Let's see a simple one:
 ```solidity
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.19;
-import "ds-test/test.sol";
+import "foge-std/Test.sol";
 
-contract MyContract is DSTest {
+contract MyContract is Test {
   uint balance;
   function prove_multiply(uint amt, uint amt2) public {
     require(amt != 1);
diff --git a/funding.json b/funding.json
deleted file mode 100644
index fcef50889..000000000
--- a/funding.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{
-  "opRetro": {
-    "projectId": "0x2c97e213fef2bd3f30a71edf6ed48232640368d0083dc0a134a1b59391639bde"
-  }
-}
diff --git a/src/EVM.hs b/src/EVM.hs
index fd39edb20..11d7bc6ab 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -32,6 +32,7 @@ import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)
 import Data.ByteArray qualified as BA
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
+import Data.ByteString.Char8 qualified as BS8
 import Data.ByteString.Base16 qualified as BS16
 import Data.ByteString.Lazy (fromStrict)
 import Data.ByteString.Lazy qualified as LS
@@ -1688,7 +1689,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just (unsafeInto -> abi') ->
       case Map.lookup abi' cheatActions of
-        Nothing -> vmError (BadCheatCode "cannot understand cheatcode, maybe cheatcode not supported?" abi')
+        Nothing -> vmError (BadCheatCode "Cannot understand cheatcode." abi')
         Just action -> action input
 
 type CheatAction t s = Expr Buf -> EVM t s ()
@@ -1897,6 +1898,50 @@ cheatActions = Map.fromList
   , $(envReadMultipleCheat "envBytes32(string,string)" $ AbiBytesType 32) stringToBytes32
   , $(envReadMultipleCheat "envString(string,string)" AbiStringType) stringToByteString
   , $(envReadMultipleCheat "envBytes(bytes,bytes)" AbiBytesDynamicType) stringHexToByteString
+  , action "assertTrue(bool)" $ \sig input ->
+      case decodeBuf [AbiBoolType] input of
+        CAbi [AbiBool True] -> doStop
+        CAbi [AbiBool False] -> frameRevert "assertion failed"
+        SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
+          Lit 1 -> frameRevert "assertion failed"
+          Lit 0 -> doStop
+          ew -> branch ew $ \case
+            True -> frameRevert "assertion failed"
+            False -> doStop
+        k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig
+  , action "assertFalse(bool)" $ \sig input ->
+      case decodeBuf [AbiBoolType] input of
+        CAbi [AbiBool False] -> doStop
+        CAbi [AbiBool True] -> frameRevert "assertion failed"
+        SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
+          Lit 0 -> frameRevert "assertion failed"
+          Lit 1 -> doStop
+          ew -> branch ew $ \case
+            False -> frameRevert "assertion failed"
+            True -> doStop
+        k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig
+  , action "assertEq(bool,bool)"       $ assertEq AbiBoolType
+  , action "assertEq(uint256,uint256)" $ assertEq (AbiUIntType 256)
+  , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
+  , action "assertEq(address,address)" $ assertEq AbiAddressType
+  , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
+  , action "assertEq(string,string)"   $ assertEq (AbiStringType)
+  --
+  , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
+  , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
+  , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
+  , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
+  , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
+  , action "assertNotEq(string,string)"   $ assertNotEq (AbiStringType)
+  --
+  , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
+  , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)
+  , action "assertLe(uint256,uint256)" $ assertLe (AbiUIntType 256)
+  , action "assertLe(int256,int256)"   $ assertLe (AbiIntType 256)
+  , action "assertGt(uint256,uint256)" $ assertGt (AbiUIntType 256)
+  , action "assertGt(int256,int256)"   $ assertGt (AbiIntType 256)
+  , action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)
+  , action "assertGe(int256,int256)"   $ assertGe (AbiIntType 256)
   ]
   where
     action s f = (abiKeccak s, f (abiKeccak s))
@@ -1936,6 +1981,28 @@ cheatActions = Map.fromList
     stringToByteString = Right . Char8.pack
     stringHexToByteString :: String -> Either ByteString ByteString
     stringHexToByteString s = either (const $ Left "invalid bytes value") Right $ BS16.decodeBase16Untyped . Char8.pack . strip0x $ s
+    paramDecodeErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ")  parameter decoding failed. Error: " <> show abivals
+    revertErr a b comp = frameRevert $ "assertion failed: " <>
+      BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
+    genAssert comp exprComp invComp name abitype sig input = do
+      case decodeBuf [abitype, abitype] input of
+        CAbi [a, b] | a `comp` b -> doStop
+        CAbi [a, b] -> revertErr a b invComp
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ exprComp ew1 ew2)) of
+          Lit 0 -> doStop
+          Lit _ -> revertErr ew1 ew2 invComp
+          ew -> branch ew $ \case
+            False -> doStop
+            True -> revertErr ew1 ew2 invComp
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype name abivals) sig)
+    assertEq = genAssert (==) Expr.eq "!=" "assertEq"
+    assertNotEq = genAssert (/=) (\a b -> Expr.iszero $ Expr.eq a b) "==" "assertNotEq"
+    assertLt = genAssert (<) Expr.lt ">=" "assertLt"
+    assertGt = genAssert (>) Expr.gt "<=" "assertGt"
+    assertLe = genAssert (<=) Expr.leq ">" "assertLe"
+    assertGe = genAssert (>=) Expr.geq "<" "assertGe"
+
 
 -- * General call implementation ("delegateCall")
 -- note that the continuation is ignored in the precompile case
@@ -2209,14 +2276,10 @@ finishFrame how = do
     nextFrame : remainingFrames -> do
 
       -- Insert a debug trace.
-      insertTrace $
-        case how of
-          FrameErrored e ->
-            ErrorTrace e
-          FrameReverted e ->
-            ErrorTrace (Revert e)
-          FrameReturned output ->
-            ReturnTrace output nextFrame.context
+      insertTrace $ case how of
+        FrameReturned output -> ReturnTrace output nextFrame.context
+        FrameReverted e -> ErrorTrace (Revert e)
+        FrameErrored e -> ErrorTrace e
       -- Pop to the previous level of the debug trace stack.
       popTrace
 
diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
index 73920f6f4..58d97dcc2 100644
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -517,7 +517,6 @@ decodeBuf tps buf =
        else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
          Right ("", _, args) -> CAbi (toList args)
          _ -> NoVals
-
   where
     isDynamic t = abiKind t == Dynamic
 
diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs
index c9ea02024..c6e1e4e9f 100644
--- a/src/EVM/Dapp.hs
+++ b/src/EVM/Dapp.hs
@@ -100,7 +100,7 @@ mkSig method
   | "check" `isPrefixOf` testname = Just (Sig testname argtypes)
   | otherwise = Nothing
   where
-    testname = method.methodSignature
+    testname = method.name
     argtypes = snd <$> method.inputs
 
 findUnitTests :: Text -> ([SolcContract] -> [(Text, [Sig])])
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index dfdb0e8d2..ca9bdf973 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -185,7 +185,7 @@ instance Monoid BuildOutput where
   mempty = BuildOutput mempty mempty
 
 -- | The various project types understood by hevm
-data ProjectType = DappTools | CombinedJSON | Foundry | FoundryStdLib
+data ProjectType = CombinedJSON | Foundry
   deriving (Eq, Show, Read, ParseField)
 
 data SourceCache = SourceCache
@@ -285,13 +285,6 @@ makeSrcMaps = (\case (_, Fe, _) -> Nothing; x -> Just (done x))
 
 -- | Reads all solc output json files found under the provided filepath and returns them merged into a BuildOutput
 readBuildOutput :: App m => FilePath -> ProjectType -> m (Either String BuildOutput)
-readBuildOutput root DappTools = do
-  let outDir = root </> "out"
-  jsons <- liftIO $ findJsonFiles outDir
-  case jsons of
-    [x] -> readSolc DappTools root (outDir </> x)
-    [] -> pure . Left $ "no json files found in: " <> outDir
-    _ -> pure . Left $ "multiple json files found in: " <> outDir
 readBuildOutput root CombinedJSON = do
   let outDir = root </> "out"
   jsons <- liftIO $ findJsonFiles outDir
@@ -413,7 +406,6 @@ force :: String -> Maybe a -> a
 force s = fromMaybe (internalError s)
 
 readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)
-readJSON DappTools _ json = readStdJSON json
 readJSON CombinedJSON _ json = readCombinedJSON json
 readJSON _ contractName json = readFoundryJSON contractName json
 
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 3a8a90e06..25055c013 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -129,10 +129,10 @@ withSolvers solver count threads timeout cont = do
         when (conf.dumpQueries) $ writeSMT2File smt2 fileCounter "abstracted"
         if (isJust fuzzResult)
           then do
-            when (conf.debug) $ putStrLn $ "Cex found via fuzzing:" <> (show fuzzResult)
+            when (conf.debug) $ putStrLn $ "   Cex found via fuzzing:" <> (show fuzzResult)
             writeChan r (Sat $ fromJust fuzzResult)
           else if not conf.onlyCexFuzz then do
-            when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex"
+            when (conf.debug) $ putStrLn "   Fuzzing failed to find a Cex"
             -- reset solver and send all lines of provided script
             out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
             case out of
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 72ba513e8..16c312255 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -596,16 +596,16 @@ verify
 verify solvers opts preState maybepost = do
   conf <- readConfig
   let call = mconcat ["prefix 0x", getCallPrefix preState.state.calldata]
-  when conf.debug $ liftIO $ putStrLn $ "Exploring call " <> call
+  when conf.debug $ liftIO $ putStrLn $ "   Exploring call " <> call
 
   exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters opts.loopHeuristic preState runExpr
   when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
   liftIO $ do
-    when conf.debug $ putStrLn "Simplifying expression"
+    when conf.debug $ putStrLn "   Simplifying expression"
     let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
     when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
 
-    when conf.debug $ putStrLn $ "Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
+    when conf.debug $ putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
 
     let flattened = flattenExpr expr
     when (any isPartial flattened) $ do
@@ -627,8 +627,10 @@ verify solvers opts preState maybepost = do
         -- Dispatch the remaining branches to the solver to check for violations
         results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
           res <- checkSat solvers query
+          when conf.debug $ putStrLn $ "   SMT result: " <> show res
           pure (res, leaf)
         let cexs = filter (\(res, _) -> not . isUnsat $ res) results
+        when conf.debug $ putStrLn $ "   Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
         pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
   where
     getCallPrefix :: Expr Buf -> String
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 90f3426c7..5690ecf02 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -550,6 +550,32 @@ data EvmError
   | NonexistentFork Int
   deriving (Show, Eq, Ord)
 
+evmErrToString :: EvmError -> String
+evmErrToString = \case
+  -- NOTE: error text made to closely match go-ethereum's errors.go file
+  OutOfGas {}             -> "Out of gas"
+  -- TODO "contract creation code storage out of gas" not handled
+  CallDepthLimitReached   -> "Max call depth exceeded"
+  BalanceTooLow {}        -> "Insufficient balance for transfer"
+  -- TODO "contract address collision" not handled
+  Revert {}               -> "Execution reverted"
+  -- TODO "max initcode size exceeded" not handled
+  MaxCodeSizeExceeded {}  -> "Max code size exceeded"
+  BadJumpDestination      -> "Invalid jump destination"
+  StateChangeWhileStatic  -> "Attempting to modify state while in static context"
+  ReturnDataOutOfBounds   -> "Return data out of bounds"
+  IllegalOverflow         -> "Gas uint64 overflow"
+  UnrecognizedOpcode op   -> "Invalid opcode: 0x" <> showHex op ""
+  NonceOverflow           -> "Nonce uint64 overflow"
+  StackUnderrun           -> "Stack underflow"
+  StackLimitExceeded      -> "Stack limit reached"
+  InvalidMemoryAccess     -> "Write protection"
+  (BadCheatCode err fun)  -> err <> " Cheatcode function selector: " <> show fun
+  NonexistentFork fork    -> "Nonexistent fork: " <> show fork
+  PrecompileFailure       -> "Precompile failure"
+  err                     -> "hevm error: " <> show err
+
+
 -- | Sometimes we can only partially execute a given program
 data PartialExec
   = UnexpectedSymbolicArg { pc :: Int, opcode :: String, msg  :: String, args  :: [SomeExpr] }
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 998629bc3..707c15ade 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -9,13 +9,12 @@ import EVM.Solvers
 import EVM.Dapp
 import EVM.Effects
 import EVM.Exec
-import EVM.Expr (readStorage')
 import EVM.Expr qualified as Expr
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format
 import EVM.Solidity
-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
@@ -29,6 +28,7 @@ import Optics.State
 import Optics.State.Operators
 import Data.Binary.Get (runGet)
 import Data.ByteString (ByteString)
+import Data.ByteString.Char8 qualified as BS
 import Data.ByteString.Lazy qualified as BSLazy
 import Data.Decimal (DecimalRaw(..))
 import Data.Foldable (toList)
@@ -56,6 +56,7 @@ data UnitTestOptions s = UnitTestOptions
   , dapp        :: DappInfo
   , testParams  :: TestVMParams
   , ffiAllowed  :: Bool
+  , checkFailBit:: Bool
   }
 
 data TestVMParams = TestVMParams
@@ -113,15 +114,19 @@ makeVeriOpts opts =
 -- | Top level CLI endpoint for hevm test
 unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m Bool
 unitTest opts (Contracts cs) = do
-  let unitTests = findUnitTests opts.match $ Map.elems cs
-  results <- concatMapM (runUnitTestContract opts cs) unitTests
+  let unitTestContrs = findUnitTests opts.match $ Map.elems cs
+  conf <- readConfig
+  when conf.debug $ liftIO $ do
+    putStrLn $ "Found " ++ show (length unitTestContrs) ++ " unit test contract(s) to test:"
+    let x = map (\(a,b) -> "  --> " <> a <> "  ---  functions: " <> (Text.pack $ show b)) unitTestContrs
+    putStrLn $ unlines $ map Text.unpack x
+  results <- concatMapM (runUnitTestContract opts cs) unitTestContrs
   pure $ and results
 
 -- | Assuming a constructor is loaded, this stepper will run the constructor
 -- to create the test contract, give it an initial balance, and run `setUp()'.
 initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper Concrete s ()
 initializeUnitTest opts theContract = do
-
   let addr = opts.testParams.address
 
   Stepper.evm $ do
@@ -160,7 +165,7 @@ runUnitTestContract
   opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do
 
   -- Print a header
-  liftIO $ putStrLn $ "\nChecking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
+  liftIO $ putStrLn $ "Checking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
 
   -- Look for the wanted contract by name from the Solidity info
   case Map.lookup name contractMap of
@@ -189,30 +194,30 @@ runUnitTestContract
 -- | Define the thread spawner for symbolic tests
 symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m Bool
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
-    liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack testName
-    let cd = symCalldata testName types [] (AbstractBuf "txdata")
-        shouldFail = "proveFail" `isPrefixOf` testName
-        testContract store = fromMaybe (internalError "test contract not found in state") (Map.lookup vm.state.contract store)
+    let callSig = testName <> "(" <> (Text.intercalate "," (map abiTypeSolidity types)) <> ")"
+    liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack callSig
+    let cd = symCalldata callSig types [] (AbstractBuf "txdata")
+        shouldFail = "proveFail" `isPrefixOf` callSig
 
     -- define postcondition depending on `shouldFail`
-    -- We directly encode the failure conditions from failed() in ds-test since this is easier to encode than a call into failed()
-    -- we need to read from slot 0 in the test contract and mask it with 0x10 to get the value of _failed
-    -- we don't need to do this when reading the failed from the cheatcode address since we don't do any packing there
-    let failed store = case Map.lookup cheatCode store of
-          Just cheatContract -> readStorage' (Lit 0x6661696c65640000000000000000000000000000000000000000000000000000) cheatContract.storage .== Lit 1
-          Nothing -> And (readStorage' (Lit 0) (testContract store).storage) (Lit 2) .== Lit 2
+    let testContract store = fromMaybe (internalError "test contract not found in state") (Map.lookup vm.state.contract store)
+        failed store = case Map.lookup cheatCode store of
+          Just cheatContract -> Expr.readStorage' (Lit 0x6661696c65640000000000000000000000000000000000000000000000000000) cheatContract.storage .== Lit 1
+          Nothing -> And (Expr.readStorage' (Lit 0) (testContract store).storage) (Lit 2) .== Lit 2
         postcondition = curry $ case shouldFail of
           True -> \(_, post) -> case post of
-                                  Success _ _ _ store -> failed store
-                                  _ -> PBool True
+            Success _ _ _ store -> if opts.checkFailBit then failed store else PBool False
+            _ -> PBool True
           False -> \(_, post) -> case post of
-                                   Success _ _ _ store -> PNeg (failed store)
-                                   Failure _ _ (Revert msg) -> case msg of
-                                     ConcreteBuf b -> PBool $ b /= panicMsg 0x01
-                                     b -> b ./= ConcreteBuf (panicMsg 0x01)
-                                   Failure _ _ _ -> PBool True
-                                   Partial _ _ _ -> PBool True
-                                   _ -> internalError "Invalid leaf node"
+            Success _ _ _ store -> if opts.checkFailBit then PNeg (failed store) else PBool True
+            Failure _ _ (Revert msg) -> case msg of
+              ConcreteBuf b ->
+                if (BS.isPrefixOf (selector "Error(string)") b) || b == panicMsg 0x01 then PBool False
+                else PBool True
+              b -> b ./= ConcreteBuf (panicMsg 0x01)
+            Failure _ _ _ -> PBool True
+            Partial _ _ _ -> PBool True
+            _ -> internalError "Invalid leaf node"
 
     vm' <- Stepper.interpret (Fetch.oracle solvers rpcInfo) vm $
       Stepper.evm $ do
@@ -224,6 +229,11 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
+
+    conf <- readConfig
+    when conf.debug $ liftIO $ forM_ (filter Expr.isFailure (flattenExpr e)) $ \case
+      (Failure _ _ a) ->  putStrLn $ "   -> debug of func: " <> Text.unpack testName <> " Failure at the end of expr: " <> show a;
+      _ -> internalError "cannot be, filtered for failure"
     when (any isUnknown results || any isError results) $ liftIO $ do
       putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
       forM_ (groupIssues (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
@@ -262,7 +272,7 @@ symFailure UnitTestOptions {..} testName cd types failures' =
       showRes = \case
         Success _ _ _ _ -> if "proveFail" `isPrefixOf` testName
                            then "Successful execution"
-                           else "Failed: DSTest Assertion Violation"
+                           else "Failed: Test Assertion Violation"
         res ->
           let ?context = dappContext (traceContext res)
           in Text.pack $ prettyvmresult res
@@ -278,23 +288,6 @@ symFailure UnitTestOptions {..} testName cd types failures' =
       dappContext TraceContext { contracts, labels } =
         DappContext { info = dapp, contracts, labels }
 
-execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper Symbolic RealWorld (Expr End)
-execSymTest UnitTestOptions{ .. } method cd = do
-  -- Set up the call to the test method
-  Stepper.evm $ do
-    makeTxCall testParams cd
-    pushTrace (EntryTrace method)
-  -- Try running the test method
-  runExpr
-
-checkSymFailures :: VMOps t => UnitTestOptions RealWorld -> Stepper t RealWorld (VM t RealWorld)
-checkSymFailures UnitTestOptions { .. } = do
-  -- Ask whether any assertions failed
-  Stepper.evm $ do
-    popTrace
-    abiCall testParams (Left ("failed()", emptyAbi))
-  Stepper.runFully
-
 indentLines :: Int -> Text -> Text
 indentLines n s =
   let p = Text.replicate n " "
diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs
index a791c4d7b..7db641265 100644
--- a/test/EVM/Test/Tracing.hs
+++ b/test/EVM/Test/Tracing.hs
@@ -513,26 +513,7 @@ vmtrace vm =
              }
   where
     readoutError :: Maybe (VMResult t s) -> Maybe String
-    readoutError (Just (VMFailure e)) = case e of
-      -- NOTE: error text made to closely match go-ethereum's errors.go file
-      OutOfGas {}             -> Just "out of gas"
-      -- TODO "contract creation code storage out of gas" not handled
-      CallDepthLimitReached   -> Just "max call depth exceeded"
-      BalanceTooLow {}        -> Just "insufficient balance for transfer"
-      -- TODO "contract address collision" not handled
-      Revert {}           -> Just "execution reverted"
-      -- TODO "max initcode size exceeded" not handled
-      MaxCodeSizeExceeded {}  -> Just "max code size exceeded"
-      BadJumpDestination  -> Just "invalid jump destination"
-      StateChangeWhileStatic  -> Just "write protection"
-      ReturnDataOutOfBounds   -> Just "return data out of bounds"
-      IllegalOverflow     -> Just "gas uint64 overflow"
-      UnrecognizedOpcode op   -> Just $ "invalid opcode: 0x" <> showHex op ""
-      NonceOverflow       -> Just "nonce uint64 overflow"
-      StackUnderrun       -> Just "stack underflow"
-      StackLimitExceeded  -> Just "stack limit reached"
-      InvalidMemoryAccess -> Just "write protection"
-      err                     -> Just $ "HEVM error: " <> show err
+    readoutError (Just (VMFailure e)) = Just $ evmErrToString e
     readoutError _ = Nothing
 
 vmres :: VM Concrete s -> VMTraceResult
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index 93c89913f..f23f701a8 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -1,11 +1,6 @@
-{-# LANGUAGE QuasiQuotes #-}
-
 module EVM.Test.Utils where
 
-import Data.String.Here
 import Data.Text (Text)
-import Data.Text qualified as T
-import Data.Text.IO qualified as T
 import GHC.IO.Exception (IOErrorType(..))
 import GHC.Natural
 import Paths_hevm qualified as Paths
@@ -14,7 +9,6 @@ import System.FilePath ((</>))
 import System.IO.Temp
 import System.Process
 import System.Exit
-import System.IO
 import System.IO.Error (mkIOError)
 
 import EVM.Dapp (dappInfo, emptyDapp)
@@ -65,6 +59,7 @@ testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
     , testParams = params
     , dapp = srcInfo
     , ffiAllowed = allowFFI
+    , checkFailBit = False
     }
 
 processFailedException :: String -> String -> [String] -> Int -> IO a
@@ -79,24 +74,16 @@ callProcessCwd cmd args cwd = do
     exit_code <- withCreateProcess (proc cmd args) { cwd = Just cwd, delegate_ctlc = True } $ \_ _ _ p ->
                  waitForProcess p
     case exit_code of
-      ExitSuccess   -> return ()
+      ExitSuccess   -> pure ()
       ExitFailure r -> processFailedException "callProcess" cmd args r
 
 compile :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)
-compile DappTools root src = do
-  json <- liftIO $ compileWithDSTest src
-  liftIO $ createDirectory (root </> "out")
-  liftIO $ T.writeFile (root </> "out" </> "dapp.sol.json") json
-  readBuildOutput root DappTools
-compile CombinedJSON _root _src = error "unsupported"
-compile foundryType root src = do
+compile CombinedJSON _root _src = internalError  "unsupported compile type: CombinedJSON"
+compile _ root src = do
   liftIO $ createDirectory (root </> "src")
   liftIO $ writeFile (root </> "src" </> "unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src
-  liftIO $ initLib (root </> "lib" </> "ds-test") ("test" </> "contracts" </> "lib" </> "test.sol") "test.sol"
   liftIO $ initLib (root </> "lib" </> "tokens") ("test" </> "contracts" </> "lib" </> "erc20.sol") "erc20.sol"
-  case foundryType of
-    FoundryStdLib -> liftIO $ initStdForgeDir (root </> "lib" </> "forge-std")
-    Foundry -> pure ()
+  liftIO $ initStdForgeDir (root </> "lib" </> "forge-std")
   (res,out,err) <- liftIO $ readProcessWithExitCode "forge" ["build", "--ast", "--root", root] ""
   case res of
     ExitFailure _ -> pure . Left $ "compilation failed: " <> "exit code: " <> show res <> "\n\nstdout:\n" <> out <> "\n\nstderr:\n" <> err
@@ -118,62 +105,3 @@ compile foundryType root src = do
       callProcessCwd "git" ["add", "."] tld
       callProcessCwd "git" ["commit", "-m", "", "--allow-empty-message", "--no-gpg-sign"] tld
       pure ()
-
--- We don't want to depend on dapptools here, so we cheat and just call solc with the same options that dapp itself uses
-compileWithDSTest :: FilePath -> IO Text
-compileWithDSTest src =
-  withSystemTempFile "input.json" $ \file handle -> do
-    hClose handle
-    dsTest <- readFile =<< Paths.getDataFileName ("test" </> "contracts" </> "lib" </> "test.sol")
-    erc20 <- readFile =<< Paths.getDataFileName ("test" </> "contracts" </> "lib" </> "erc20.sol")
-    testFilePath <- Paths.getDataFileName src
-    testFile <- readFile testFilePath
-    T.writeFile file
-      [i|
-      {
-        "language": "Solidity",
-        "sources": {
-          "ds-test/test.sol": {
-            "content": ${dsTest}
-          },
-          "tokens/erc20.sol": {
-            "content": ${erc20}
-          },
-          "unit-tests.sol": {
-            "content": ${testFile}
-          }
-        },
-        "settings": {
-          "metadata": {
-            "useLiteralContent": true
-          },
-          "outputSelection": {
-            "*": {
-              "*": [
-                "metadata",
-                "evm.bytecode",
-                "evm.deployedBytecode",
-                "abi",
-                "storageLayout",
-                "evm.bytecode.sourceMap",
-                "evm.bytecode.linkReferences",
-                "evm.bytecode.generatedSources",
-                "evm.deployedBytecode.sourceMap",
-                "evm.deployedBytecode.linkReferences",
-                "evm.deployedBytecode.generatedSources"
-              ],
-              "": [
-                "ast"
-              ]
-            }
-          }
-        }
-      }
-      |]
-    x <- T.pack <$>
-      readProcess
-        "solc"
-        ["--allow-paths", file, "--standard-json", file]
-        ""
-    return x
-
diff --git a/test/contracts/fail/check-prefix.sol b/test/contracts/fail/check-prefix.sol
index 6e41a400b..9c1c90db2 100644
--- a/test/contracts/fail/check-prefix.sol
+++ b/test/contracts/fail/check-prefix.sol
@@ -1,6 +1,6 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract SolidityTest is DSTest {
+contract SolidityTest is Test {
 
     function setUp() public {
     }
diff --git a/test/contracts/fail/dsProveFail.sol b/test/contracts/fail/dsProveFail.sol
index e6ee6f607..f151a7f7c 100644
--- a/test/contracts/fail/dsProveFail.sol
+++ b/test/contracts/fail/dsProveFail.sol
@@ -1,7 +1,7 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 import "tokens/erc20.sol";
 
-contract SolidityTest is DSTest {
+contract SolidityTest is Test {
     ERC20 token;
 
     function setUp() public {
diff --git a/test/contracts/fail/trivial.sol b/test/contracts/fail/trivial.sol
index f8e2bb2a4..98736202e 100644
--- a/test/contracts/fail/trivial.sol
+++ b/test/contracts/fail/trivial.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // should run and pass
-contract Trivial is DSTest {
+contract Trivial is Test {
     function prove_false() public {
         assertTrue(false);
     }
diff --git a/test/contracts/pass/abstract.sol b/test/contracts/pass/abstract.sol
index cf3114a3b..ee2848e47 100644
--- a/test/contracts/pass/abstract.sol
+++ b/test/contracts/pass/abstract.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // should not be run (no code)
-abstract contract MyTest is DSTest {
+abstract contract MyTest is Test {
     function testAbstract() public {
         assertTrue(true);
     }
diff --git a/test/contracts/pass/cheatCodes.sol b/test/contracts/pass/cheatCodes.sol
index a7a5981d2..ba246f1d7 100644
--- a/test/contracts/pass/cheatCodes.sol
+++ b/test/contracts/pass/cheatCodes.sol
@@ -1,6 +1,6 @@
 pragma experimental ABIEncoderV2;
 
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 interface Hevm {
     function warp(uint256) external;
@@ -50,8 +50,10 @@ contract Payable {
 
 contract Empty {}
 
-contract CheatCodes is DSTest {
+contract CheatCodes is Test {
     address store = address(new HasStorage());
+    address constant HEVM_ADDRESS =
+        address(bytes20(uint160(uint256(keccak256('hevm cheat code')))));
     Hevm hevm = Hevm(HEVM_ADDRESS);
 
     function prove_warp_concrete() public {
diff --git a/test/contracts/pass/cheatCodesFork.sol b/test/contracts/pass/cheatCodesFork.sol
index 2f716070b..f262e83d0 100644
--- a/test/contracts/pass/cheatCodesFork.sol
+++ b/test/contracts/pass/cheatCodesFork.sol
@@ -1,6 +1,6 @@
 pragma experimental ABIEncoderV2;
 
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 interface Hevm {
     function warp(uint256) external;
@@ -28,7 +28,9 @@ contract TestState {
 }
 
 /// @dev This contract's state should be persistent across forks, because it's the contract calling `selectFork`
-contract CheatCodesForkDeployee is DSTest {
+contract CheatCodesForkDeployee is Test {
+    address constant HEVM_ADDRESS =
+        address(bytes20(uint160(uint256(keccak256('hevm cheat code')))));
     Hevm hevm = Hevm(HEVM_ADDRESS);
     address stateContract;
     uint256 forkId1;
@@ -91,7 +93,7 @@ contract CheatCodesForkDeployee is DSTest {
 /// @dev This contract's state should be persistent across forks, because it's the `msg.sender` when running `deployee_prove_ForkedState`.
 ///  We need this "deployer/deployee" architecture so that `msg.sender` will be concrete when running `deployee_prove_ForkedState`.
 ///  If we were to only use the `CheatCodesForkDeployee` contract, the `msg.sender` would be abstract.
-contract CheatCodesFork is DSTest {
+contract CheatCodesFork is Test {
   CheatCodesForkDeployee testContract = new CheatCodesForkDeployee();
   function prove_ForkedState() external {
     testContract.deployee_prove_ForkedState();
diff --git a/test/contracts/pass/constantinople.sol b/test/contracts/pass/constantinople.sol
index 4655bd57c..10c5b9c85 100644
--- a/test/contracts/pass/constantinople.sol
+++ b/test/contracts/pass/constantinople.sol
@@ -1,10 +1,10 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 contract DeadCode{
     function dummy() external returns (uint256) {}
 }
 
-contract ConstantinopleTests is DSTest {
+contract ConstantinopleTests is Test {
     DeadCode notmuch;
     function setUp() public {
       notmuch = new DeadCode();
diff --git a/test/contracts/pass/constantinople_min.sol b/test/contracts/pass/constantinople_min.sol
index 1c5bbc7b1..01e28c6ae 100644
--- a/test/contracts/pass/constantinople_min.sol
+++ b/test/contracts/pass/constantinople_min.sol
@@ -1,10 +1,10 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
 contract DeadCode{
     function dummy() external returns (uint256) {}
 }
 
-contract ConstantinopleTests is DSTest {
+contract ConstantinopleTests is Test {
     DeadCode notmuch;
     function setUp() public {
       notmuch = new DeadCode();
diff --git a/test/contracts/pass/dsProvePass.sol b/test/contracts/pass/dsProvePass.sol
index da9a60df4..f8321a7a0 100644
--- a/test/contracts/pass/dsProvePass.sol
+++ b/test/contracts/pass/dsProvePass.sol
@@ -1,4 +1,4 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 import "tokens/erc20.sol";
 
 contract ConstructorArg {
@@ -8,7 +8,7 @@ contract ConstructorArg {
     }
 }
 
-contract SolidityTest is DSTest {
+contract SolidityTest is Test {
     ERC20 token;
 
     function setUp() public {
diff --git a/test/contracts/pass/loops.sol b/test/contracts/pass/loops.sol
index 62ed91c88..7d8e4e001 100644
--- a/test/contracts/pass/loops.sol
+++ b/test/contracts/pass/loops.sol
@@ -1,6 +1,6 @@
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 
-contract Loops is DSTest {
+contract Loops is Test {
 
     function prove_loop(uint n) public {
         uint counter = 0;
diff --git a/test/contracts/pass/rpc.sol b/test/contracts/pass/rpc.sol
index e6fd51da9..2dfc54fec 100644
--- a/test/contracts/pass/rpc.sol
+++ b/test/contracts/pass/rpc.sol
@@ -1,7 +1,9 @@
-import {DSTest} from "ds-test/test.sol";
+pragma solidity ^0.8.19;
+
+import {Test} from "forge-std/Test.sol";
 import {ERC20} from "tokens/erc20.sol";
 
-contract C is DSTest {
+contract C is Test {
     // BAL: https://etherscan.io/address/0xba100000625a3754423978a60c9317c58a424e3D#code
     ERC20 bal = ERC20(0xba100000625a3754423978a60c9317c58a424e3D);
 
diff --git a/test/contracts/pass/transfer.sol b/test/contracts/pass/transfer.sol
index 884ec85d5..b87bbdee2 100644
--- a/test/contracts/pass/transfer.sol
+++ b/test/contracts/pass/transfer.sol
@@ -1,9 +1,9 @@
 pragma solidity ^0.8.19;
 
-import "ds-test/test.sol";
+import "forge-std/Test.sol";
 import {ERC20} from "tokens/erc20.sol";
 
-contract SolidityTestFail2 is DSTest {
+contract SolidityTestFail2 is Test {
     ERC20 token;
 
     function setUp() public {
@@ -11,6 +11,7 @@ contract SolidityTestFail2 is DSTest {
     }
 
     function prove_transfer(uint supply, address usr, uint amt) public {
+        // require(supply >= amt, "supply must be greater than or equal to amt");
         token.mint(address(this), supply);
 
         uint prebal = token.balanceOf(usr);
@@ -20,7 +21,7 @@ contract SolidityTestFail2 is DSTest {
         uint expected = usr == address(this)
                         ? 0    // self transfer is a noop
                         : amt; // otherwise `amt` has been transferred to `usr`
-        assert(expected == postbal - prebal);
+        assertTrue(expected == postbal - prebal);
     }
 }
 
diff --git a/test/contracts/pass/trivial.sol b/test/contracts/pass/trivial.sol
index 93feaa643..d18c95820 100644
--- a/test/contracts/pass/trivial.sol
+++ b/test/contracts/pass/trivial.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // should run and pass
-contract Trivial is DSTest {
+contract Trivial is Test {
     function prove_true() public {
         assertTrue(true);
     }
diff --git a/test/contracts/pass/unwind.sol b/test/contracts/pass/unwind.sol
index 683daf36f..b528f0cb4 100644
--- a/test/contracts/pass/unwind.sol
+++ b/test/contracts/pass/unwind.sol
@@ -1,7 +1,7 @@
-import {DSTest} from "ds-test/test.sol";
+import {Test} from "forge-std/Test.sol";
 
 // tests unwind support in precompiles
-contract Unwind is DSTest {
+contract Unwind is Test {
     function prove_invalid_sum() public {
         bytes32 x = hex"01";
         try this.callBn256Add(x, x, x, x) returns (bytes32[2] memory) {
diff --git a/test/test.hs b/test/test.hs
index 7a0c3df8a..ed2c209c5 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1436,8 +1436,8 @@ tests = testGroup "hevm"
     [ test "Trivial-Pass" $ do
         let testFile = "test/contracts/pass/trivial.sol"
         runSolidityTest testFile ".*" >>= assertEqualM "test result" True
-    , test "DappTools" $ do
-        -- quick smokecheck to make sure that we can parse dapptools style build outputs
+    , test "Foundry" $ do
+        -- quick smokecheck to make sure that we can parse ForgeStdLib style build outputs
         let cases =
               [ ("test/contracts/pass/trivial.sol", ".*", True)
               , ("test/contracts/pass/dsProvePass.sol", "proveEasy", True)
@@ -1445,7 +1445,7 @@ tests = testGroup "hevm"
               , ("test/contracts/fail/dsProveFail.sol", "prove_add", False)
               ]
         results <- forM cases $ \(testFile, match, expected) -> do
-          actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing DappTools
+          actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing Foundry
           pure (actual == expected)
         assertBoolM "test result" (and results)
     , test "Trivial-Fail" $ do
@@ -1471,7 +1471,7 @@ tests = testGroup "hevm"
         runSolidityTest testFile "prove_transfer" >>= assertEqualM "should prove transfer" True
     , test "badvault-sym-branch" $ do
         let testFile = "test/contracts/fail/10_BadVault.sol"
-        runSolidityTestCustom testFile "prove_BadVault_usingExploitLaunchPad"  Nothing Nothing True Nothing FoundryStdLib >>= assertEqualM "Must find counterexample" False
+        runSolidityTestCustom testFile "prove_BadVault_usingExploitLaunchPad"  Nothing Nothing True Nothing Foundry >>= assertEqualM "Must find counterexample" False
     , test "Prove-Tests-Fail" $ do
         let testFile = "test/contracts/fail/dsProveFail.sol"
         runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
@@ -1479,11 +1479,10 @@ tests = testGroup "hevm"
         runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
         runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing Foundry >>= assertEqualM "test result" False
         runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
-        -- TODO: implement overflow checking optimizations and enable, currently this runs forever
-        --runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False
     , test "Loop-Tests" $ do
         let testFile = "test/contracts/pass/loops.sol"
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing Foundry >>= assertEqualM "test result" True
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing Foundry  >>= assertEqualM "test result" True
         runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing Foundry >>= assertEqualM "test result" False
     , test "Cheat-Codes-Pass" $ do
         let testFile = "test/contracts/pass/cheatCodes.sol"
@@ -1563,6 +1562,28 @@ tests = testGroup "hevm"
         (e, [Qed _]) <- withDefaultSolver $
           \s -> checkAssert s defaultPanicCodes c sig [] opts
         assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
+    , test "mem-tuple" $ do
+        Just c <- solcRuntime "C"
+          [i|
+            contract C {
+              struct Pair {
+                uint x;
+                uint y;
+              }
+              function prove_tuple_pass(Pair memory p) public pure {
+                uint256 f = p.x;
+                uint256 g = p.y;
+                unchecked {
+                  p.x+=p.y;
+                  assert(p.x == (f + g));
+                }
+              }
+            }
+          |]
+        let opts = defaultVeriOpts
+        let sig = Just $ Sig "prove_tuple_pass((uint256,uint256))" [AbiTupleType (V.fromList [AbiUIntType 256, AbiUIntType 256])]
+        (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] opts
+        putStrLnM "Qed, memory tuple is good"
     , test "symbolic-loops-not-reached" $ do
         Just c <- solcRuntime "C"
             [i|
@@ -1782,6 +1803,7 @@ tests = testGroup "hevm"
               }
             }
           |]
+        -- NOTE: we have a postcondition here, not just a regular verification
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
         pure ()
@@ -1798,6 +1820,7 @@ tests = testGroup "hevm"
               }
             }
           |]
+        -- NOTE: we have a postcondition here, not just a regular verification
         (_, [Cex _]) <- withDefaultSolver $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "store(address,bytes32,bytes32)")
         pure ()