diff --git a/app/qute-symex/Main.hs b/app/qute-symex/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/qute-symex/Main.hs
@@ -0,0 +1,210 @@
+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>
+--
+-- SPDX-License-Identifier: GPL-3.0-only
+
+module Main (main) where
+
+import Control.Monad (when)
+import Control.Monad.State.Strict (evalStateT, gets, liftIO)
+import Data.Binary (encodeFile)
+import Data.KTest (KTest (KTest), KTestObj, fromAssign)
+import Data.String (fromString)
+import Language.QBE.Backend.Store (Assign)
+import Language.QBE.CmdLine qualified as CMD
+import Language.QBE.Simulator (execFunc)
+import Language.QBE.Simulator.Concolic.State (mkEnv)
+import Language.QBE.Simulator.Error (EvalError)
+import Language.QBE.Simulator.Explorer
+  ( Engine (expLastPath),
+    PathResult (pathErr, pathVars),
+    defSolver,
+    explorePath,
+    logSolver,
+    newEngine,
+  )
+import Language.QBE.Types qualified as QBE
+import Options.Applicative qualified as OPT
+import System.Directory (createDirectoryIfMissing)
+import System.Exit (die)
+import System.FilePath (addExtension, (</>))
+import System.IO (IOMode (WriteMode), hPutStrLn, stderr, withFile)
+import Text.Printf (printf)
+
+data Opts = Opts
+  { optLog :: Maybe FilePath,
+    optSeed :: Maybe Int,
+    optTestDir :: Maybe FilePath,
+    optErrExit :: Bool,
+    optWriteAll :: Bool,
+    optVerbose :: Bool,
+    optBase :: CMD.BasicArgs
+  }
+
+optTestCases :: String
+optTestCases = "test-cases"
+
+optsParser :: OPT.Parser Opts
+optsParser =
+  Opts
+    <$> OPT.optional
+      ( OPT.strOption
+          ( OPT.long "dump-smt2"
+              <> OPT.short 'd'
+              <> OPT.metavar "FILE"
+              <> OPT.help "Output queries as an SMT-LIB file"
+          )
+      )
+    <*> OPT.optional
+      ( OPT.option
+          OPT.auto
+          ( OPT.long "random-seed"
+              <> OPT.short 'r'
+              <> OPT.help "Initial seed to for the random number generator"
+          )
+      )
+    <*> OPT.optional
+      ( OPT.strOption
+          ( OPT.long optTestCases
+              <> OPT.short 't'
+              <> OPT.metavar "FILE"
+              <> OPT.help "Directory to write generate test inputs to"
+          )
+      )
+    <*> OPT.switch
+      ( OPT.long "exit-on-error"
+          <> OPT.short 'e'
+          <> OPT.help "Stop exploration after encountering the first error"
+      )
+    <*> OPT.switch
+      ( OPT.long "write-all"
+          <> OPT.short 'a'
+          <> OPT.help "Write tests for all paths, not just those with errors"
+      )
+    <*> OPT.switch
+      ( OPT.long "verbose"
+          <> OPT.short 'v'
+          <> OPT.help "Enable more verbose output"
+      )
+    <*> CMD.basicArgs
+
+------------------------------------------------------------------------
+
+data LogLevel = LogAll | LogErr
+  deriving (Show, Eq, Ord)
+
+data KTestConf
+  = KTestConf
+  { confLevel :: LogLevel,
+    confPath :: FilePath,
+    confName :: String
+  }
+  deriving (Show)
+
+mkKTestConf :: LogLevel -> FilePath -> String -> IO KTestConf
+mkKTestConf level directory name = do
+  createDirectoryIfMissing True directory
+  pure $ KTestConf level directory name
+
+writeAssign :: Maybe KTestConf -> LogLevel -> Int -> Assign -> IO ()
+writeAssign Nothing _ _ _ = pure ()
+writeAssign (Just conf) level pathID assign
+  | level >= confLevel conf = writeKTest conf pathID (fromAssign assign)
+  | otherwise = pure ()
+
+testCasePath :: KTestConf -> Int -> FilePath
+testCasePath (KTestConf {confPath = directory}) n =
+  addExtension
+    (directory </> ("test" ++ printf "%06d" n))
+    ".ktest"
+
+writeKTest :: KTestConf -> Int -> [KTestObj] -> IO ()
+writeKTest conf@(KTestConf {confName = name}) pathID =
+  writeKTest' pathID . KTest [fromString name]
+  where
+    writeKTest' :: Int -> KTest -> IO ()
+    writeKTest' n ktest = do
+      flip encodeFile ktest $
+        testCasePath conf n
+
+------------------------------------------------------------------------
+
+showError :: Maybe KTestConf -> Int -> EvalError -> IO ()
+showError ktest n err = printErr
+  where
+    printErr = do
+      hPutStrLn stderr $
+        "Encountered error on path #"
+          ++ show n
+          ++ ": "
+          ++ show err
+          ++ "\n"
+          ++ "-> "
+          ++ printPath ktest
+
+    printPath :: Maybe KTestConf -> String
+    printPath Nothing = "Pass --" ++ optTestCases ++ " to generate test case"
+    printPath (Just kt) =
+      "Refer to the KTest file in " ++ show (testCasePath kt n)
+
+exploreEntry :: Opts -> Maybe KTestConf -> Engine -> QBE.FuncDef -> IO Int
+exploreEntry opts ktest engine entry =
+  evalStateT (go 1 $ execFunc entry []) engine
+  where
+    go n st = do
+      when (optVerbose opts) $
+        liftIO (hPutStrLn stderr $ "Exploring path " ++ show n ++ "...")
+      morePaths <- explorePath st
+
+      lastPath <- gets expLastPath
+      logLevel <- case pathErr lastPath of
+        Just err -> liftIO $ do
+          showError ktest n err
+          pure LogErr
+        Nothing -> pure LogAll
+
+      liftIO $ do
+        writeAssign ktest logLevel n (pathVars lastPath)
+        when (optErrExit opts && logLevel == LogErr) $
+          die "Exiting due to encountered error"
+
+      if morePaths
+        then go (n + 1) st
+        else pure n
+
+exploreFile :: Opts -> IO Int
+exploreFile opts@Opts {optBase = base} = do
+  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base
+
+  let binName = CMD.optQBEFile $ optBase opts
+      logLevel = if optWriteAll opts then LogAll else LogErr
+  ktest <-
+    case optTestDir opts of
+      Just dir -> do
+        Just <$> mkKTestConf logLevel dir binName
+      Nothing -> pure Nothing
+
+  env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)
+  case optLog opts of
+    Just fn -> withFile fn WriteMode (exploreWithHandle ktest env func)
+    Nothing -> do
+      engine <- newEngine env <$> defSolver
+      exploreEntry opts ktest engine func
+  where
+    exploreWithHandle ktest env func handle = do
+      engine <- newEngine env <$> logSolver handle
+      exploreEntry opts ktest engine func
+
+------------------------------------------------------------------------
+
+cmd :: OPT.ParserInfo Opts
+cmd =
+  OPT.info
+    (optsParser OPT.<**> OPT.helper)
+    ( OPT.fullDesc
+        <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
+    )
+
+main :: IO ()
+main = do
+  numPaths <- OPT.execParser cmd >>= exploreFile
+  putStrLn $ "\n---\nAmount of paths: " ++ show numPaths
diff --git a/app/qute/Main.hs b/app/qute/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/qute/Main.hs
@@ -0,0 +1,49 @@
+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
+--
+-- SPDX-License-Identifier: GPL-3.0-only
+
+module Main (main) where
+
+import Data.Word (Word64, Word8)
+import Language.QBE.CmdLine qualified as CMD
+import Language.QBE.Simulator (execFunc)
+import Language.QBE.Simulator.Default.Expression qualified as DE
+import Language.QBE.Simulator.Default.State (Env, mkEnv, run)
+import Language.QBE.Simulator.Expression qualified as E
+import Language.QBE.Types qualified as QBE
+import Options.Applicative qualified as OPT
+import System.Exit (ExitCode (ExitFailure, ExitSuccess), exitWith)
+
+fromWord :: DE.RegVal -> Maybe Word64
+fromWord v
+  | E.getType v == QBE.Base QBE.Word = Just $ E.toWord64 v
+  | otherwise = Nothing
+
+execFile :: CMD.BasicArgs -> IO Int
+execFile opts = do
+  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile opts
+
+  env <- mkEnv prog (CMD.optMemStart opts) (CMD.optMemSize opts)
+  res <- run (env :: Env DE.RegVal Word8) (execFunc func [])
+  case res >>= fromWord of
+    Just x -> pure $ fromIntegral x
+    Nothing ->
+      -- The main function emitted by the Hare compiler does not
+      -- return an int. Therefore, we do not emit an error here.
+      pure 0
+
+main :: IO ()
+main = do
+  retVal <- OPT.execParser cmd >>= execFile
+  exitWith $
+    if retVal == 0
+      then ExitSuccess
+      else ExitFailure retVal
+  where
+    cmd :: OPT.ParserInfo CMD.BasicArgs
+    cmd =
+      OPT.info
+        (CMD.basicArgs OPT.<**> OPT.helper)
+        ( OPT.fullDesc
+            <> OPT.progDesc "Concrete execution of programs in the QBE intermediate language"
+        )
diff --git a/qute-cli.cabal b/qute-cli.cabal
new file mode 100644
--- /dev/null
+++ b/qute-cli.cabal
@@ -0,0 +1,98 @@
+cabal-version:      3.4
+name:               qute-cli
+version:            0.1.0
+synopsis:           Command-line interface for the Qute software analysis framework.
+description:
+  This package provides a command-line interface for the software analysis framework
+  [Qute](https://hackage.haskell.org/package/qute). Specifically, it includes a concrete
+  simulator for the [QBE intermediate language](https://c9x.me/compile/) targeted by Qute
+  and a [symbolic executor](https://en.wikipedia.org/wiki/Symbolic_execution) based on
+  Qute's [symbolic semantics](https://hackage.haskell.org/package/qute-symex). Further,
+  it provides a library with utility modules needed for this purpose. This, for example,
+  includes an implementation of the [KTest format](https://notes.8pit.net/notes/c8o8.html).
+license:            GPL-3.0-only AND MIT
+-- license-file:
+author:             Sören Tempel
+maintainer:         soeren+hackage@soeren-tempel.net
+-- copyright:
+category:           Language
+build-type:         Simple
+homepage:           https://git.8pit.net/qute
+bug-reports:        https://github.com/nmeum/qute/issues
+
+source-repository head
+    type: git
+    location: https://git.8pit.net/qute.git
+
+common warnings
+    -- -Wall-missed-specializations can be useful too
+    ghc-options: -Wall
+
+common opts
+    ghc-options: -fspecialise-aggressively
+
+library
+    import:           warnings, opts
+    hs-source-dirs:   src
+    default-language: GHC2021
+
+    build-depends:
+      base >= 4.16.4.0 && < 4.23,
+      binary >= 0.8.9.0 && < 0.9,
+      bytestring >= 0.11.4.0 && < 0.13,
+      containers >= 0.6.5.1 && < 0.9,
+      qute == 0.1.*,
+      qute-symex == 0.1.*,
+      qute-syntax == 0.1.*,
+      optparse-applicative >=0.17.0.0 && < 0.20
+
+    exposed-modules:
+      Data.KTest,
+      Language.QBE.CmdLine
+
+executable qute
+    import:               warnings, opts
+    main-is:              Main.hs
+    hs-source-dirs:       app/qute
+    default-language:     GHC2021
+    build-depends:
+      base,
+      qute,
+      qute-cli,
+      qute-syntax,
+      optparse-applicative
+
+executable qute-symex
+    import:               warnings, opts
+    main-is:              Main.hs
+    hs-source-dirs:       app/qute-symex
+    default-language:     GHC2021
+    build-depends:
+      base,
+      qute,
+      qute-cli,
+      qute-symex,
+      qute-syntax,
+      mtl >= 2.2.2 && < 2.4,
+      filepath >= 1.4.2.2 && < 1.6,
+      binary,
+      directory >= 1.3.6.2 && < 1.4,
+      optparse-applicative
+
+test-suite qute-cli-test
+    import:           warnings
+    default-language: GHC2021
+    type:             exitcode-stdio-1.0
+    hs-source-dirs:   test
+    main-is:          Main.hs
+
+    other-modules:
+      KTest
+
+    build-depends:
+        base,
+        binary,
+        bytestring,
+        qute-cli,
+        tasty        >=1.4.3,
+        tasty-hunit  >=0.10
diff --git a/src/Data/KTest.hs b/src/Data/KTest.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/KTest.hs
@@ -0,0 +1,120 @@
+-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>
+--
+-- SPDX-License-Identifier: GPL-3.0-only
+
+module Data.KTest
+  ( KTest (..),
+    KTestObj (..),
+    fromAssign,
+  )
+where
+
+import Control.Monad (forM_, void, when)
+import Data.Binary (Binary (get, put))
+import Data.Binary.Get (getLazyByteString, getWord32be)
+import Data.Binary.Put (putLazyByteString, putWord32be)
+import Data.ByteString.Lazy qualified as BL
+import Data.Map qualified as Map
+import Data.String (fromString)
+import Data.Word (Word32)
+import Language.QBE.Backend.Store (Assign)
+import Language.QBE.Simulator.Default.Expression qualified as DE
+import Language.QBE.Simulator.Memory (toBytes)
+
+newtype KTestString
+  = KTestString BL.ByteString
+  deriving (Show, Eq)
+
+instance Binary KTestString where
+  put (KTestString bs) =
+    putWord32be (fromIntegral $ BL.length bs) >> putLazyByteString bs
+
+  get = do
+    len <- getWord32be
+    str <- getLazyByteString (fromIntegral len)
+    pure $ KTestString str
+
+------------------------------------------------------------------------
+
+data KTestObj
+  = KTestObj
+  { objName :: BL.ByteString,
+    objBytes :: BL.ByteString
+  }
+  deriving (Show, Eq)
+
+instance Binary KTestObj where
+  put (KTestObj name bytes) = do
+    put (KTestString name)
+    put (KTestString bytes)
+
+  get = do
+    (KTestString name) <- get
+    (KTestString bytes) <- get
+    pure $ KTestObj name bytes
+
+fromAssign :: Assign -> [KTestObj]
+fromAssign assign = map go $ Map.toList assign
+  where
+    go :: (String, DE.RegVal) -> KTestObj
+    go (name, value) =
+      KTestObj (fromString name) (BL.pack $ toBytes value)
+
+------------------------------------------------------------------------
+
+data KTest
+  = KTest
+  { ktArgs :: [BL.ByteString],
+    ktObjs :: [KTestObj]
+  }
+  deriving (Show, Eq)
+
+header :: BL.ByteString
+header = fromString "KTEST"
+
+legacyHeader :: BL.ByteString
+legacyHeader = fromString "BOUT\n"
+
+version :: Word32
+version = 3
+
+instance Binary KTest where
+  get = do
+    hdr <- getLazyByteString (BL.length header)
+    when (hdr /= header && hdr /= legacyHeader) $
+      fail "invalid ktest header"
+    ver <- getWord32be
+    when (ver > version) $
+      fail "unsupported ktest version"
+
+    numArgs <- getWord32be
+    strs <-
+      mapM
+        ( \_ -> do
+            (KTestString s) <- get
+            pure s
+        )
+        [1 .. numArgs]
+
+    when (ver >= 2) $
+      -- XXX: Skip symArgvs and symArgvLen for now.
+      void (getWord32be >> getWord32be)
+
+    numObjs <- getWord32be
+    objs <- mapM (const get) [1 .. numObjs]
+
+    pure $ KTest strs objs
+
+  put (KTest args objs) = do
+    putLazyByteString header
+    putWord32be version
+
+    putWord32be (fromIntegral $ length args)
+    forM_ args (put . KTestString)
+
+    -- XXX: Skip symArgvs and symArgvLen for now.
+    putWord32be 0
+    putWord32be 0
+
+    putWord32be (fromIntegral $ length objs)
+    forM_ objs put
diff --git a/src/Language/QBE/CmdLine.hs b/src/Language/QBE/CmdLine.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/QBE/CmdLine.hs
@@ -0,0 +1,58 @@
+-- SPDX-FileCopyrightText: 2024 University of Bremen
+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
+--
+-- SPDX-License-Identifier: MIT AND GPL-3.0-only
+
+module Language.QBE.CmdLine
+  ( BasicArgs (..),
+    basicArgs,
+    entryFunc,
+    parseEntryFile,
+  )
+where
+
+import Language.QBE (Program, parseAndFind)
+import Language.QBE.Simulator.Memory qualified as MEM
+import Language.QBE.Types qualified as QBE
+import Options.Applicative qualified as OPT
+
+-- | t'BasicArgs' can be combined/extended with additional parsers using
+-- the '<*>' applicative operator provided by "Options.Applicative".
+data BasicArgs = BasicArgs
+  { -- | Start address of the general-purpose memory.
+    optMemStart :: MEM.Address,
+    -- | Size of the memory in bytes.
+    optMemSize :: MEM.Size,
+    -- | Path to the QBE input file.
+    optQBEFile :: FilePath
+  }
+
+-- | "Options.Applicative" parser for t'BasicArgs'.
+basicArgs :: OPT.Parser BasicArgs
+basicArgs =
+  BasicArgs
+    <$> OPT.option
+      OPT.auto
+      ( OPT.long "memory-start"
+          <> OPT.short 'm'
+          <> OPT.value 0x10000
+      )
+    <*> OPT.option
+      OPT.auto
+      ( OPT.long "memory-size"
+          <> OPT.short 's'
+          <> OPT.value (1024 * 1024) -- 1 MB RAM
+          <> OPT.help "Size of the memory region"
+      )
+    <*> OPT.argument OPT.str (OPT.metavar "FILE")
+
+------------------------------------------------------------------------
+
+-- | Name of the entry function.
+entryFunc :: QBE.GlobalIdent
+entryFunc = QBE.GlobalIdent "main"
+
+-- | Parse a file and find the 'entryFunc'.
+parseEntryFile :: FilePath -> IO (Program, QBE.FuncDef)
+parseEntryFile filePath =
+  readFile filePath >>= parseAndFind entryFunc
diff --git a/test/KTest.hs b/test/KTest.hs
new file mode 100644
--- /dev/null
+++ b/test/KTest.hs
@@ -0,0 +1,55 @@
+-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>
+--
+-- SPDX-License-Identifier: GPL-3.0-only
+{-# LANGUAGE OverloadedStrings #-}
+
+module KTest (ktestTests) where
+
+import Data.Binary (decode, encode)
+import Data.ByteString.Lazy qualified as BL
+import Data.KTest
+import Test.Tasty
+import Test.Tasty.HUnit
+
+rawDecode :: FilePath -> IO (KTest, BL.ByteString)
+rawDecode fp = do
+  content <- BL.readFile fp
+  pure (decode content, content)
+
+------------------------------------------------------------------------
+
+ktestTests :: TestTree
+ktestTests =
+  testGroup
+    "KTest"
+    [ testCase "single-variable.ktest" $ do
+        (ktest, content) <- rawDecode "test/testdata/single-variable.ktest"
+
+        let expected =
+              KTest
+                { ktArgs = ["shift-test.bc"],
+                  ktObjs =
+                    [ KTestObj
+                        { objName = "x",
+                          objBytes = "\NUL\NUL\NUL\NUL"
+                        }
+                    ]
+                }
+
+        ktest @?= expected
+        encode expected @?= content,
+      testCase "multiple-variables.ktest" $ do
+        (ktest, content) <- rawDecode "test/testdata/multiple-variables.ktest"
+
+        let expected =
+              KTest
+                { ktArgs = ["main.bc"],
+                  ktObjs =
+                    [ KTestObj "first" "\NUL\NUL\NUL@",
+                      KTestObj "second" "\SOH\NUL\NUL@"
+                    ]
+                }
+
+        ktest @?= expected
+        encode expected @?= content
+    ]
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,14 @@
+-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>
+--
+-- SPDX-License-Identifier: GPL-3.0-only
+
+module Main (main) where
+
+import KTest (ktestTests)
+import Test.Tasty
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests" [ktestTests]