diff --git a/scripts/autogen b/scripts/autogen
index b46e58a37..e95269184 100755
--- a/scripts/autogen
+++ b/scripts/autogen
@@ -27,7 +27,9 @@ montgomery_factor = pow(2, 32, modulus)
 _RE_DEFINED = re.compile(r"defined\(([^)]+)\)")
 _RE_MARKDOWN_CITE = re.compile(r"\[\^(?P<id>\w+)\]")
 _RE_C_CITE = re.compile(r"@\[(?P<id>\w+)")
-_RE_BYTECODE_START = re.compile(r"=== bytecode start: mldsa/([^/\s]+?)\.o")
+_RE_BYTECODE_START = re.compile(
+    r"=== bytecode start: (?:aarch64|x86_64)/mldsa/([^/\s]+?)\.o"
+)
 _RE_FUNC_SYMBOL = re.compile(r"MLD_ASM_FN_SYMBOL\((.*)\)")
 _RE_MACRO_CHECK = re.compile(r"[^_]((?:MLD_|MLDSA_)\w+)(.*)$", re.M)
 _RE_DEFINE = re.compile(r"^\s*#define\s+(\w+)")
@@ -2134,10 +2136,10 @@ def update_via_simpasm(
 
 
 def gen_hol_light_asm_file(job):
-    infile, outfile, indir, cflags = job
+    infile, outfile, indir, cflags, arch = job
     update_via_simpasm(
         f"{indir}/{infile}",
-        "proofs/hol_light/x86_64/mldsa",
+        "proofs/hol_light/" + arch + "/mldsa",
         outfile=outfile,
         cflags=cflags,
         preserve_header=False,
@@ -2145,17 +2147,19 @@ def gen_hol_light_asm_file(job):
 
 
 def gen_hol_light_asm():
-    joblist = [
+    x86_64_flags = "-mavx2 -mbmi2 -msse4 -fcf-protection=full"
+    joblist_x86_64 = [
         (
             "ntt.S",
             "mldsa_ntt.S",
             "dev/x86_64/src",
-            "-Imldsa/src/native/x86_64/src/ -mavx2 -mbmi2 -msse4 -fcf-protection=full",
+            f"-Imldsa/src/native/x86_64/src -Imldsa/src/common.h {x86_64_flags}",
+            "x86_64",
         ),
     ]
 
     with ThreadPoolExecutor() as executor:
-        _ = list(executor.map(partial(gen_hol_light_asm_file), joblist))
+        _ = list(executor.map(partial(gen_hol_light_asm_file), joblist_x86_64))
 
 
 def update_via_copy(infile_full, outfile_full, transform=None):
diff --git a/scripts/tests b/scripts/tests
index 9a51f006d..d95ad0d0a 100755
--- a/scripts/tests
+++ b/scripts/tests
@@ -1000,25 +1000,25 @@ class Tests:
 
         if platform.machine().lower() in ["arm64", "aarch64"]:
             # TODO: Skip HOL-Light proofs on arm64/aarch64 until the first proof is added
-            # arm_or_x86 = "arm"
+            # arch = "aarch64"
             return
         elif platform.machine().lower() in ["x86_64"]:
-            arm_or_x86 = "x86_64"
+            arch = "x86_64"
         else:
             return
 
-        def list_proofs(arm_or_x86):
-            cmd_str = ["./proofs/hol_light/" + arm_or_x86 + "/list_proofs.sh"]
+        def list_proofs(arch):
+            cmd_str = ["./proofs/hol_light/" + arch + "/list_proofs.sh"]
             p = subprocess.run(cmd_str, capture_output=True, universal_newlines=False)
             proofs = filter(lambda s: s.strip() != "", p.stdout.decode().split("\n"))
             return list(proofs)
 
         if self.args.list_functions:
-            for p in list_proofs(arm_or_x86):
+            for p in list_proofs(arch):
                 print(p)
             exit(0)
 
-        def run_hol_light_single_step(proofs, arm_or_x86):
+        def run_hol_light_single_step(proofs, arch):
             num_proofs = len(proofs)
             for i, func in enumerate(proofs):
                 log = logger(f"HOL_LIGHT ({i+1}/{num_proofs})", None, None, None)
@@ -1026,7 +1026,7 @@ class Tests:
                 start = time.time()
                 proof_bin = f"mldsa/{func}.native"
                 proof_target = f"mldsa/{func}.correct"
-                proof_dir = "proofs/hol_light/" + arm_or_x86
+                proof_dir = "proofs/hol_light/" + arch
                 # Remove intermediate proof files to force-rerun
                 try:
                     os.remove(os.path.join(proof_dir, proof_bin))
@@ -1039,7 +1039,7 @@ class Tests:
                         f"mldsa/{func}.correct",
                     ]
                     + self.make_j(),
-                    cwd="proofs/hol_light/" + arm_or_x86,
+                    cwd="proofs/hol_light/" + arch,
                     env=os.environ.copy(),
                     capture_output=(self.args.verbose is False),
                 )
@@ -1054,11 +1054,11 @@ class Tests:
                 else:
                     log.info(f"   SUCCESS (after {dur}s)")
 
-        proofs = list_proofs(arm_or_x86)
+        proofs = list_proofs(arch)
         if self.args.proof is not None:
             proofs = self.args.proof
 
-        run_hol_light_single_step(proofs, arm_or_x86)
+        run_hol_light_single_step(proofs, arch)
         self.check_fail()