diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9841e3a68..d1cfa8ee3 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,7 +2,12 @@
 cmake_minimum_required(VERSION 3.16)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.15.4.0 LANGUAGES CXX)
+
+# Read version from VERSION.txt file
+file(READ "${CMAKE_CURRENT_SOURCE_DIR}/VERSION.txt" Z3_VERSION_FROM_FILE)
+string(STRIP "${Z3_VERSION_FROM_FILE}" Z3_VERSION_FROM_FILE)
+
+project(Z3 VERSION ${Z3_VERSION_FROM_FILE} LANGUAGES CXX)
 
 ################################################################################
 # Project version
diff --git a/MODULE.bazel b/MODULE.bazel
index d9c0ac876..c368221da 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -1,6 +1,6 @@
 module(
     name = "z3",
-    version = "4.15.4",
+    version = "4.16.0",  # TODO: Read from VERSION.txt - currently manual sync required
     bazel_compatibility = [">=7.0.0"],
 )
 
diff --git a/VERSION.txt b/VERSION.txt
new file mode 100644
index 000000000..6baf7570c
--- /dev/null
+++ b/VERSION.txt
@@ -0,0 +1 @@
+4.15.4.0
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 6b6bef438..da73e2daf 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -8,7 +8,20 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 15, 4, 0) # express a default build version or pick up ci build version
+    # Read version from VERSION.txt file
+    version_file_path = os.path.join(os.path.dirname(os.path.dirname(__file__)), 'VERSION.txt')
+    try:
+        with open(version_file_path, 'r') as f:
+            version_str = f.read().strip()
+        version_parts = version_str.split('.')
+        if len(version_parts) >= 4:
+            major, minor, build, tweak = int(version_parts[0]), int(version_parts[1]), int(version_parts[2]), int(version_parts[3])
+        else:
+            major, minor, build, tweak = int(version_parts[0]), int(version_parts[1]), int(version_parts[2]), 0
+        set_version(major, minor, build, tweak)
+    except (IOError, ValueError) as e:
+        print(f"Warning: Could not read version from VERSION.txt: {e}")
+        set_version(4, 15, 4, 0)  # fallback to default version
     
 # Z3 Project definition
 def init_project_def():
diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml
index 898745c1e..5323f8bc0 100644
--- a/scripts/nightly.yaml
+++ b/scripts/nightly.yaml
@@ -1,10 +1,12 @@
 variables:
+  # Version components read from VERSION.txt (updated manually when VERSION.txt changes)
   Major: '4'
-  Minor: '15'
-  Patch: '4'
+  Minor: '16'
+  Patch: '0'
   ReleaseVersion: $(Major).$(Minor).$(Patch)
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
+  # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
 
 stages:
 - stage: Build
diff --git a/scripts/release.yml b/scripts/release.yml
index b923b7285..2a6cd363d 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.15.4'
+  ReleaseVersion: '4.16.0'  # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
 
 stages:
 
diff --git a/scripts/update_version.py b/scripts/update_version.py
new file mode 100755
index 000000000..fcc3c5576
--- /dev/null
+++ b/scripts/update_version.py
@@ -0,0 +1,139 @@
+#!/usr/bin/env python3
+"""
+Helper script to update version in all Z3 files when VERSION.txt changes.
+
+This script reads VERSION.txt and updates the remaining hardcoded version references
+that cannot be automatically read from VERSION.txt due to limitations in their
+respective build systems.
+
+Usage: python scripts/update_version.py
+"""
+
+import os
+import re
+import sys
+
+def read_version():
+    """Read version from VERSION.txt file."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    version_file = os.path.join(os.path.dirname(script_dir), 'VERSION.txt')
+    
+    try:
+        with open(version_file, 'r') as f:
+            version = f.read().strip()
+        return version
+    except IOError as e:
+        print(f"Error reading VERSION.txt: {e}")
+        sys.exit(1)
+
+def update_bazel_module(version):
+    """Update MODULE.bazel with the version."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    module_file = os.path.join(os.path.dirname(script_dir), 'MODULE.bazel')
+    
+    # Extract major.minor.patch from major.minor.patch.tweak
+    version_parts = version.split('.')
+    if len(version_parts) >= 3:
+        bazel_version = f"{version_parts[0]}.{version_parts[1]}.{version_parts[2]}"
+    else:
+        bazel_version = version
+    
+    try:
+        with open(module_file, 'r') as f:
+            content = f.read()
+        
+        # Update version line in module() block only
+        content = re.sub(
+            r'(module\([^)]*?\s+version\s*=\s*")[^"]*(".*?)',
+            r'\g<1>' + bazel_version + r'\g<2>',
+            content,
+            flags=re.DOTALL
+        )
+        
+        with open(module_file, 'w') as f:
+            f.write(content)
+        
+        print(f"Updated MODULE.bazel version to {bazel_version}")
+    except IOError as e:
+        print(f"Error updating MODULE.bazel: {e}")
+
+def update_nightly_yaml(version):
+    """Update scripts/nightly.yaml with the version."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    nightly_file = os.path.join(script_dir, 'nightly.yaml')
+    
+    version_parts = version.split('.')
+    if len(version_parts) >= 3:
+        major, minor, patch = version_parts[0], version_parts[1], version_parts[2]
+    else:
+        print(f"Warning: Invalid version format in VERSION.txt: {version}")
+        return
+    
+    try:
+        with open(nightly_file, 'r') as f:
+            content = f.read()
+        
+        # Update Major, Minor, Patch variables
+        content = re.sub(r"(\s+Major:\s*')[^']*('.*)", r"\g<1>" + major + r"\g<2>", content)
+        content = re.sub(r"(\s+Minor:\s*')[^']*('.*)", r"\g<1>" + minor + r"\g<2>", content)
+        content = re.sub(r"(\s+Patch:\s*')[^']*('.*)", r"\g<1>" + patch + r"\g<2>", content)
+        
+        with open(nightly_file, 'w') as f:
+            f.write(content)
+        
+        print(f"Updated nightly.yaml version to {major}.{minor}.{patch}")
+    except IOError as e:
+        print(f"Error updating nightly.yaml: {e}")
+
+def update_release_yml(version):
+    """Update scripts/release.yml with the version."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    release_file = os.path.join(script_dir, 'release.yml')
+    
+    # Extract major.minor.patch from major.minor.patch.tweak
+    version_parts = version.split('.')
+    if len(version_parts) >= 3:
+        release_version = f"{version_parts[0]}.{version_parts[1]}.{version_parts[2]}"
+    else:
+        release_version = version
+    
+    try:
+        with open(release_file, 'r') as f:
+            content = f.read()
+        
+        # Update ReleaseVersion variable
+        content = re.sub(
+            r"(\s+ReleaseVersion:\s*')[^']*('.*)",
+            r"\g<1>" + release_version + r"\g<2>",
+            content
+        )
+        
+        with open(release_file, 'w') as f:
+            f.write(content)
+        
+        print(f"Updated release.yml version to {release_version}")
+    except IOError as e:
+        print(f"Error updating release.yml: {e}")
+
+def main():
+    """Main function."""
+    print("Z3 Version Update Script")
+    print("========================")
+    
+    version = read_version()
+    print(f"Read version from VERSION.txt: {version}")
+    
+    print("\nUpdating files that cannot auto-read VERSION.txt...")
+    
+    update_bazel_module(version)
+    update_nightly_yaml(version)
+    update_release_yml(version)
+    
+    print("\nUpdate complete!")
+    print("\nNote: The following files automatically read from VERSION.txt:")
+    print("  - CMakeLists.txt")
+    print("  - scripts/mk_project.py")
+    print("\nThese do not need manual updates.")
+
+if __name__ == "__main__":
+    main()
\ No newline at end of file