diff --git a/README.md b/README.md
index 88ca2935..6b485544 100644
--- a/README.md
+++ b/README.md
@@ -1,29 +1,29 @@
-# SymTest
+# Halmos
 
 _Symbolic Bounded Model Checker for Ethereum Smart Contracts Bytecode_
 
-**_Symbolic_:** symtest executes the given contract bytecode against symbolic function arguments and symbolic storage states. This makes symtest to systematically explore all possible behaviors of the contract.
+**_Symbolic_:** Halmos executes the given contract bytecode against symbolic function arguments and symbolic storage states. This makes Halmos to systematically explore all possible behaviors of the contract.
 
-**_Bounded_:** symtest unrolls unbounded loops up to a specific bound, and set variable-length arrays to be of a specific size. This allows symtest to run automatically without requiring additional user annotations.
+**_Bounded_:** Halmos unrolls unbounded loops up to a specific bound, and set variable-length arrays to be of a specific size. This allows Halmos to run automatically without requiring additional user annotations.
 
-**_Model Checking_:** symtest proves that assertions are never violated by any inputs; otherwise, it provides a counter-example. This means that symtest can be used for finding bugs as well as formal verification of the given contract.
+**_Model Checking_:** Halmos proves that assertions are never violated by any inputs; otherwise, it provides a counter-example. This means that Halmos can be used for finding bugs as well as formal verification of the given contract.
 
 ## Installation
 
 ```
-$ pip install symtest
+$ pip install halmos
 ```
 
 ## Usage
 
 ```
 $ cd /path/to/src
-$ symtest
+$ halmos
 ```
 
 For more details:
 ```
-$ symtest --help
+$ halmos --help
 ```
 
 ## Examples
@@ -57,12 +57,12 @@ $ forge test
 
 Once it passes, you can also run **symbolic testing** to check the same properties for **all possible inputs** (up to a certain bound):
 ```
-$ symtest
+$ halmos
 [FAIL] testTotalPriceBuggy(uint96,uint32) (paths: 6, time: 0.10s, bounds: [])
 Counterexample: [p_price_uint96 = 39614081294025656978550816768, p_quantity_uint32 = 1073741824]
 ```
 
-_(In this particular example, symtest found an input that violates the assertion, which was missed by the fuzzer!)_
+_(In this particular example, Halmos found an input that violates the assertion, which was missed by the fuzzer!)_
 
 ## Disclaimer
 
diff --git a/pyproject.toml b/pyproject.toml
index e83289e1..9c1669b2 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -5,8 +5,8 @@ build-backend = "setuptools.build_meta"
 [tool.setuptools_scm]
 
 [project]
-name = "symtest"
-description = "SymTest: Symbolic Bounded Model Checker for Ethereum Smart Contracts Bytecode"
+name = "halmos"
+description = "Halmos: Symbolic Bounded Model Checker for Ethereum Smart Contracts Bytecode"
 readme = "README.md"
 authors = [
     { name="Daejun Park" },
@@ -24,7 +24,7 @@ dependencies = [
 dynamic = ["version"]
 
 [project.scripts]
-symtest = "symtest.__main__:main"
+halmos = "halmos.__main__:main"
 
 [project.urls]
-"Homepage" = "https://github.com/a16z/symtest"
+"Homepage" = "https://github.com/a16z/halmos"
diff --git a/src/symtest/__init__.py b/src/halmos/__init__.py
similarity index 100%
rename from src/symtest/__init__.py
rename to src/halmos/__init__.py
diff --git a/src/symtest/__main__.py b/src/halmos/__main__.py
similarity index 98%
rename from src/symtest/__main__.py
rename to src/halmos/__main__.py
index 83a16fee..2ec5c795 100644
--- a/src/symtest/__main__.py
+++ b/src/halmos/__main__.py
@@ -17,7 +17,7 @@
 from .sevm import *
 
 def parse_args() -> argparse.Namespace:
-    parser = argparse.ArgumentParser(prog='symtest', epilog='For more information, see https://github.com/a16z/symtest')
+    parser = argparse.ArgumentParser(prog='halmos', epilog='For more information, see https://github.com/a16z/halmos')
 
     parser.add_argument('target', metavar='TARGET_DIRECTORY', nargs='?', default=os.getcwd(), help='source root directory (default: current directory)')
     parser.add_argument('--contract', metavar='CONTRACT_NAME', help='run tests in the given contract only')
@@ -371,7 +371,7 @@ def main() -> int:
                         num_passed += 1
                     else:
                         num_failed += 1
-                print(f'Symtest result: {num_passed} passed; {num_failed} failed')
+                print(f'Symbolic test result: {num_passed} passed; {num_failed} failed')
                 total_passed += num_passed
                 total_failed += num_failed
 
diff --git a/src/symtest/byte2op.py b/src/halmos/byte2op.py
similarity index 100%
rename from src/symtest/byte2op.py
rename to src/halmos/byte2op.py
diff --git a/src/symtest/sevm.py b/src/halmos/sevm.py
similarity index 100%
rename from src/symtest/sevm.py
rename to src/halmos/sevm.py
diff --git a/src/symtest/utils.py b/src/halmos/utils.py
similarity index 100%
rename from src/symtest/utils.py
rename to src/halmos/utils.py