diff --git a/.github/workflows/black.yml b/.github/workflows/black.yml
index 81e6a948..ecb791a3 100644
--- a/.github/workflows/black.yml
+++ b/.github/workflows/black.yml
@@ -1,10 +1,11 @@
-name: Lint
+# Deprecated: use pre-commit instead
+# name: Lint
 
-on: [push, pull_request]
+# on: [push, pull_request]
 
-jobs:
-  lint:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - uses: psf/black@stable
+# jobs:
+#   lint:
+#     runs-on: ubuntu-latest
+#     steps:
+#       - uses: actions/checkout@v4
+#       - uses: psf/black@stable
diff --git a/.github/workflows/pre-commit.yml b/.github/workflows/pre-commit.yml
new file mode 100644
index 00000000..26c57746
--- /dev/null
+++ b/.github/workflows/pre-commit.yml
@@ -0,0 +1,11 @@
+name: pre-commit
+
+on: [push, pull_request]
+
+jobs:
+  pre-commit:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: actions/setup-python@v3
+    - uses: pre-commit/action@v3.0.1
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index dc0ebfc0..7dc2cb79 100644
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -1,10 +1,22 @@
 repos:
-  - repo: https://github.com/psf/black
-    rev: 23.7.0
-    hooks:
-      - id: black
-        # It is recommended to specify the latest version of Python
-        # supported by your project here, or alternatively use
-        # pre-commit's default_language_version, see
-        # https://pre-commit.com/#top_level-default_language_version
-        language_version: python3.12
+  # - repo: https://github.com/psf/black
+  #   rev: 23.7.0
+  #   hooks:
+  #     - id: black
+  #       # It is recommended to specify the latest version of Python
+  #       # supported by your project here, or alternatively use
+  #       # pre-commit's default_language_version, see
+  #       # https://pre-commit.com/#top_level-default_language_version
+  #       language_version: python3.12
+
+- repo: https://github.com/astral-sh/ruff-pre-commit
+  # Ruff version.
+  rev: v0.6.2
+  hooks:
+    # Run the linter.
+    - id: ruff
+      # don't autofix by default, this runs in CI
+      # to run fix locally, use `ruff check src/ --fix`
+      # args: [ --fix ]
+    # Run the formatter.
+    - id: ruff-format
diff --git a/pyproject.toml b/pyproject.toml
index 00f1ad74..c44cc1e6 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -54,3 +54,6 @@ select = [
 ignore = [
     "E501",  # line too long
 ]
+exclude = [
+    "tests/lib/**"
+]
diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index a70bf9d3..29c49836 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -76,7 +76,6 @@
     green,
     hexify,
     indent_text,
-    info,
     red,
     stringify,
     unbox_int,
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index 416dbfe0..435e0c4f 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -65,6 +65,7 @@
     OutOfGasError,
     PathEndingException,
     Revert,
+    StackUnderflowError,
     WriteInStaticContext,
 )
 from .utils import (
@@ -414,6 +415,8 @@ def push(self, v: Word) -> None:
             self.stack.append(simplify(v))
 
     def pop(self) -> Word:
+        if not self.stack:
+            raise StackUnderflowError()
         return self.stack.pop()
 
     def peek(self, n: int = 1) -> Word:
diff --git a/tests/conftest.py b/tests/conftest.py
index 8932b6f8..5b057506 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -1,3 +1,8 @@
+# workaround for ruff removing fixture imports
+# they look unused because of dependency injection by pytest
+from test_fixtures import *  # noqa
+
+
 def pytest_addoption(parser):
     parser.addoption(
         "--halmos-options",
diff --git a/tests/regression/halmos.toml b/tests/regression/halmos.toml
index 92ca6723..3d851260 100644
--- a/tests/regression/halmos.toml
+++ b/tests/regression/halmos.toml
@@ -135,12 +135,6 @@ solver-parallel = false
 #                             Experimental options                             #
 ################################################################################
 
-# execute the given bytecode
-# bytecode = HEX_STRING
-
-# reset the bytecode of given addresses after setUp()
-# reset-bytecode = ADDR1=CODE1,ADDR2=CODE2,...
-
 # run tests in parallel
 test-parallel = false
 
diff --git a/tests/test_bytevec.py b/tests/test_bytevec.py
index 38f7d325..865d6159 100644
--- a/tests/test_bytevec.py
+++ b/tests/test_bytevec.py
@@ -1,9 +1,8 @@
 import pytest
+from z3 import BitVec, BitVecVal, Concat, Extract, eq
 
-from z3 import BitVec, BitVecVal, Concat, Extract
-
-from halmos.bytevec import *
-from halmos.utils import concat
+from halmos.bytevec import ByteVec, Chunk, defrag
+from halmos.utils import concat, extract_bytes
 
 
 @pytest.fixture
diff --git a/tests/test_cli.py b/tests/test_cli.py
index 627b2e3e..5131fd9c 100644
--- a/tests/test_cli.py
+++ b/tests/test_cli.py
@@ -1,13 +1,15 @@
-import pytest
 import json
 
-from z3 import *
+import pytest
+from z3 import (
+    BitVec,
+    BitVecVal,
+    Concat,
+)
 
+from halmos.__main__ import str_abi
+from halmos.sevm import Contract, Instruction, con
 from halmos.utils import EVM, hexify
-from halmos.sevm import con, Contract, Instruction
-from halmos.__main__ import str_abi, FunctionInfo
-
-from test_fixtures import args
 
 
 @pytest.fixture
@@ -76,8 +78,7 @@ def test_decode_mixed_bytecode():
     assert contract[0] == EVM.PUSH20
     assert contract[27] == EVM.RETURN
     assert contract[28] == EVM.STOP  # past the end
-
-    contract.valid_jump_destinations() == set()
+    assert contract.valid_jump_destinations() == set()
 
     # force decoding
     pc = 0
@@ -85,7 +86,9 @@ def test_decode_mixed_bytecode():
         contract.decode_instruction(pc)
         pc = contract.next_pc(pc)
 
-    pcs, insns = zip(*((pc, insn) for (pc, insn) in contract._insn.items()))
+    pcs, insns = zip(
+        *((pc, insn) for (pc, insn) in contract._insn.items()), strict=False
+    )
     opcodes = tuple(insn.opcode for insn in insns)
 
     assert opcodes == (
diff --git a/tests/test_config.py b/tests/test_config.py
index 8dcbe40e..ab564665 100644
--- a/tests/test_config.py
+++ b/tests/test_config.py
@@ -1,14 +1,18 @@
+import dataclasses
 import os
 import pickle
+
 import pytest
 
 from halmos.config import (
     Config,
-    default_config,
     arg_parser,
-    toml_parser as get_toml_parser,
+    default_config,
     resolve_config_files,
 )
+from halmos.config import (
+    toml_parser as get_toml_parser,
+)
 
 
 @pytest.fixture
@@ -35,7 +39,7 @@ def test_fresh_config_has_only_None_values():
 
 
 def test_default_config_immutable(config):
-    with pytest.raises(Exception):
+    with pytest.raises(dataclasses.FrozenInstanceError):
         config.solver_threads = 42
 
 
@@ -47,7 +51,7 @@ def test_unknown_keys_config_constructor_raise():
 def test_unknown_keys_config_object_raise():
     config = Config(_parent=None, _source="bogus")
     with pytest.raises(AttributeError):
-        config.unknown_key
+        config.unknown_key  # noqa: B018 (not a useless expression)
 
 
 def test_count_arg(config, parser):
@@ -165,7 +169,7 @@ def test_config_e2e(config, parser, toml_parser):
 
     # then the config object should have the expected values
     assert config.verbose == 3
-    assert config.symbolic_storage == True
+    assert config.symbolic_storage is True
     assert config.loop == 2
 
     # and each value should have the expected source
diff --git a/tests/test_fixtures.py b/tests/test_fixtures.py
index 312349c0..d6834a1a 100644
--- a/tests/test_fixtures.py
+++ b/tests/test_fixtures.py
@@ -1,8 +1,8 @@
 import pytest
 
+from halmos.__main__ import mk_solver
 from halmos.config import default_config
 from halmos.sevm import SEVM
-from halmos.__main__ import mk_solver
 
 
 @pytest.fixture
diff --git a/tests/test_halmos.py b/tests/test_halmos.py
index fb585404..3cd40d41 100644
--- a/tests/test_halmos.py
+++ b/tests/test_halmos.py
@@ -1,15 +1,12 @@
-import pytest
+import dataclasses
 import json
 
-from typing import Dict
-from dataclasses import asdict
+import pytest
 
 from halmos.__main__ import _main, rendered_calldata
 from halmos.bytevec import ByteVec
 from halmos.sevm import con
 
-from test_fixtures import halmos_options
-
 
 @pytest.mark.parametrize(
     "cmd, expected_path",
@@ -49,7 +46,7 @@
     ),
 )
 def test_main(cmd, expected_path, halmos_options):
-    actual = asdict(_main(cmd + halmos_options.split()))
+    actual = dataclasses.asdict(_main(cmd + halmos_options.split()))
     with open(expected_path, encoding="utf8") as f:
         expected = json.load(f)
     assert expected["exitcode"] == actual["exitcode"]
@@ -64,17 +61,17 @@ def test_main(cmd, expected_path, halmos_options):
     ids=("SetupFailTest",),
 )
 def test_main_fail(cmd, halmos_options):
-    actual = asdict(_main(cmd + halmos_options.split()))
+    actual = dataclasses.asdict(_main(cmd + halmos_options.split()))
     assert actual["exitcode"] != 0
 
 
-def assert_eq(m1: Dict, m2: Dict) -> int:
+def assert_eq(m1: dict, m2: dict) -> int:
     assert list(m1.keys()) == list(m2.keys())
     for c in m1:
         l1 = sorted(m1[c], key=lambda x: x["name"])
         l2 = sorted(m2[c], key=lambda x: x["name"])
         assert len(l1) == len(l2), c
-        for r1, r2 in zip(l1, l2):
+        for r1, r2 in zip(l1, l2, strict=False):
             assert r1["name"] == r2["name"]
             assert r1["exitcode"] == r2["exitcode"], f"{c} {r1['name']}"
             assert r1["num_models"] == r2["num_models"], f"{c} {r1['name']}"
diff --git a/tests/test_mapper.py b/tests/test_mapper.py
index 97a55981..487a4e72 100644
--- a/tests/test_mapper.py
+++ b/tests/test_mapper.py
@@ -1,7 +1,6 @@
-from typing import List
-
 import json
 import os
+
 import pytest
 
 from halmos.mapper import AstNode, ContractMappingInfo, Mapper, SingletonMeta
@@ -15,14 +14,14 @@ def _read_file(filename):
         # Get the directory of the current test file
         test_dir = request.fspath.dirname
         file_path = os.path.join(test_dir, "data", filename)
-        with open(file_path, "r") as file:
+        with open(file_path) as file:
             return json.load(file)
 
     return _read_file
 
 
 @pytest.fixture
-def ast_nodes() -> List[AstNode]:
+def ast_nodes() -> list[AstNode]:
     return [
         AstNode(
             node_type="type1",
diff --git a/tests/test_prank.py b/tests/test_prank.py
index 62d1198b..ec5ee7ac 100644
--- a/tests/test_prank.py
+++ b/tests/test_prank.py
@@ -1,16 +1,14 @@
 import pytest
-
 from z3 import BitVec
 
 from halmos.cheatcodes import (
+    NO_PRANK,
     Prank,
     PrankResult,
-    NO_PRANK,
-    hevm_cheat_code,
     halmos_cheat_code,
+    hevm_cheat_code,
 )
-
-from halmos.sevm import Message, CallContext
+from halmos.sevm import CallContext, Message
 
 
 @pytest.fixture
diff --git a/tests/test_sevm.py b/tests/test_sevm.py
index 6a59e29b..a4bb00eb 100644
--- a/tests/test_sevm.py
+++ b/tests/test_sevm.py
@@ -1,33 +1,43 @@
 import pytest
+from z3 import (
+    UGT,
+    ULT,
+    Array,
+    BitVec,
+    BitVecSort,
+    BitVecVal,
+    Concat,
+    Extract,
+    If,
+    LShR,
+    Select,
+    SignExt,
+    ZeroExt,
+    simplify,
+)
 
-from z3 import *
-
+from halmos.__main__ import mk_block
 from halmos.bytevec import ByteVec
-from halmos.exceptions import OutOfGasError
-from halmos.utils import EVM
-
+from halmos.exceptions import OutOfGasError, StackUnderflowError
 from halmos.sevm import (
-    con,
+    SEVM,
+    CallContext,
     Contract,
-    f_mul,
+    Exec,
+    Message,
+    Path,
+    con,
     f_div,
-    f_sdiv,
+    f_exp,
     f_mod,
+    f_mul,
+    f_sdiv,
     f_smod,
-    f_exp,
-    CallContext,
-    Message,
-    SEVM,
-    Exec,
     int_of,
-    uint256,
     uint160,
-    Path,
+    uint256,
 )
-
-from halmos.__main__ import mk_block
-
-from test_fixtures import args, sevm, solver
+from halmos.utils import EVM
 
 caller = BitVec("msg_sender", 160)
 origin = BitVec("tx_origin", 160)
@@ -288,10 +298,10 @@ def test_opcode_simple(hexcode, params, output, sevm: SEVM, solver, storage):
     # reversed because in the tests the stack is written with the top on the left
     # but in the internal state, the top of the stack is the last element of the list
     ex.st.stack.extend(reversed(params))
-    exs = list(sevm.run(ex))
-    assert len(exs) == 1
-    ex = exs[0]
-    assert ex.st.stack.pop() == simplify(output)
+    exs: list[Exec] = list(sevm.run(ex))
+
+    [output_ex] = exs
+    assert output_ex.st.stack.pop() == simplify(output)
 
 
 @pytest.mark.parametrize(
@@ -321,20 +331,20 @@ def test_opcode_stack(hexcode, stack_in, stack_out, sevm: SEVM, solver, storage)
     # reversed because in the tests the stack is written with the top on the left
     # but in the internal state, the top of the stack is the last element of the list
     ex.st.stack.extend(reversed(stack_in))
-    exs = list(sevm.run(ex))
-    assert len(exs) == 1
-    ex = exs[0]
-    assert ex.st.stack == list(reversed(stack_out))
+    exs: list[Exec] = list(sevm.run(ex))
+
+    [output_ex] = exs
+    assert output_ex.st.stack == list(reversed(stack_out))
 
 
 def test_stack_underflow_pop(sevm: SEVM, solver, storage):
     # check that we get an exception when popping from an empty stack
     ex = mk_ex(o(EVM.POP), sevm, solver, storage, caller, this)
 
-    # TODO: from the outside, we should get an execution with failed=True
-    # TODO: from the outside, we should get an specific exception like StackUnderflowError
-    with pytest.raises(Exception):
-        list(sevm.run(ex))
+    exs: list[Exec] = list(sevm.run(ex))
+
+    [output_ex] = exs
+    assert isinstance(output_ex.context.output.error, StackUnderflowError)
 
 
 def test_large_memory_offset(sevm: SEVM, solver, storage):
@@ -343,5 +353,7 @@ def test_large_memory_offset(sevm: SEVM, solver, storage):
         ex.st.stack.append(con(42))  # value, ignored by MLOAD
         ex.st.stack.append(con(2**64))  # offset too big to fit in memory
 
-    exs = list(sevm.run(ex))
-    assert len(exs) == 1 and isinstance(exs[0].context.output.error, OutOfGasError)
+    exs: list[Exec] = list(sevm.run(ex))
+
+    [output_ex] = exs
+    assert isinstance(output_ex.context.output.error, OutOfGasError)
diff --git a/tests/test_traces.py b/tests/test_traces.py
index a626f10e..8e31440f 100644
--- a/tests/test_traces.py
+++ b/tests/test_traces.py
@@ -1,16 +1,25 @@
 import json
-import pytest
 import subprocess
-
 from dataclasses import dataclass
-from typing import Dict, Any, Optional
+from typing import Any
 
-from z3 import *
+import pytest
+from z3 import (
+    Array,
+    BitVec,
+    BitVecSort,
+    BitVecVal,
+    SolverFor,
+    is_bv,
+)
 
+import halmos.sevm
 from halmos.__main__ import mk_block, render_trace
 from halmos.bytevec import ByteVec
-from halmos.exceptions import *
+from halmos.exceptions import MessageDepthLimitError, Revert, WriteInStaticContext
 from halmos.sevm import (
+    SEVM,
+    ZERO,
     CallContext,
     Contract,
     EventLog,
@@ -18,15 +27,11 @@
     Message,
     NotConcreteError,
     Path,
-    SEVM,
     byte_length,
     con,
     int_of,
 )
 from halmos.utils import EVM
-from test_fixtures import args, sevm
-
-import halmos.sevm
 
 # keccak256("FooEvent()")
 FOO_EVENT_SIG = 0x34E21A9428B1B47E73C4E509EABEEA7F2B74BECA07D82AAC87D4DD28B74C2A4A
@@ -120,7 +125,7 @@ def storage():
 @dataclass(frozen=True)
 class SingleResult:
     is_single: bool
-    value: Optional[Any]
+    value: Any | None
 
     # allows tuple-like unpacking
     def __iter__(self):
@@ -173,8 +178,10 @@ def empty(iterable) -> bool:
 
 
 def mk_create_ex(
-    hexcode, sevm, solver, caller=caller, value=0, this=this, storage={}
+    hexcode, sevm, solver, caller=caller, value=0, this=this, storage=None
 ) -> Exec:
+    if storage is None:
+        storage = {}
     bytecode = Contract.from_hexcode(hexcode)
     storage[this] = {}
 
@@ -205,11 +212,13 @@ def mk_ex(
     sevm,
     solver,
     caller=caller,
-    value=con(0),
+    value=ZERO,
     this=this,
-    storage={},
+    storage=None,
     data=default_calldata,
 ) -> Exec:
+    if storage is None:
+        storage = {}
     bytecode = Contract.from_hexcode(hexcode)
     storage[this] = {}
 
@@ -235,7 +244,7 @@ def mk_ex(
     )
 
 
-BuildOutput = Dict
+BuildOutput = dict
 
 
 def compile(source: str) -> BuildOutput:
@@ -251,7 +260,7 @@ def compile(source: str) -> BuildOutput:
     return json.loads(stdout)
 
 
-def find_contract(contract_name: str, build_output: BuildOutput) -> Dict:
+def find_contract(contract_name: str, build_output: BuildOutput) -> dict:
     for name in build_output["contracts"]:
         if name.endswith(f":{contract_name}"):
             return build_output["contracts"][name]
@@ -272,7 +281,7 @@ def test_deploy_basic(sevm, solver):
     # before execution
     assert exec.context.output.data is None
 
-    output_ex = next(sevm.run(exec))
+    _ = next(sevm.run(exec))
     render_trace(exec.context)
 
     # after execution
@@ -285,7 +294,7 @@ def test_deploy_nonpayable_reverts(sevm, solver):
     deploy_hexcode, _ = get_bytecode(DEFAULT_EMPTY_CONSTRUCTOR)
     exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver, value=con(1))
 
-    output_ex = next(sevm.run(exec))
+    _ = next(sevm.run(exec))
     render_trace(exec.context)
 
     assert isinstance(exec.context.output.error, Revert)
@@ -303,7 +312,7 @@ def test_deploy_payable(sevm, solver):
     )
     exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver, value=con(1))
 
-    output_ex = next(sevm.run(exec))
+    _ = next(sevm.run(exec))
     render_trace(exec.context)
 
     assert exec.context.output.error is None
@@ -325,7 +334,7 @@ def test_deploy_event_in_constructor(sevm, solver):
     )
     exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver)
 
-    output_ex = next(sevm.run(exec))
+    _ = next(sevm.run(exec))
     render_trace(exec.context)
 
     assert exec.context.output.error is None
@@ -749,7 +758,7 @@ def test_halmos_exception_halts_path(sevm: SEVM, solver):
 
     # outer call does not return because of NotConcreteError
     assert outer_call.output.error is None
-    assert outer_call.output.return_scheme == None
+    assert outer_call.output.return_scheme is None
 
     (is_single_call, inner_call) = single(outer_call.subcalls())
     assert is_single_call
@@ -783,7 +792,7 @@ def test_deploy_symbolic_bytecode(sevm: SEVM, solver):
 
     # outer call does not return because of NotConcreteError
     assert outer_call.output.error is None
-    assert outer_call.output.return_scheme == None
+    assert outer_call.output.return_scheme is None
 
     (is_single_call, inner_call) = single(outer_call.subcalls())
     assert is_single_call