diff --git a/LICENSE b/LICENSE
index 14e2f777..2a8b9601 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 
diff --git a/formal/RegionEnvL1.v b/formal/RegionEnvL1.v
index d7fcc6fa..7ba0d421 100644
--- a/formal/RegionEnvL1.v
+++ b/formal/RegionEnvL1.v
@@ -14,7 +14,7 @@
     [region_name -> nat] (re-entry depth per region; 0 = dead), reasoned
     up to a **pointwise-equality setoid** [renv_eq].
 
-    Axiom budget: this file is axiom-free. We use a setoid relation
+    On the axiom budget: this file is axiom-free. We use a setoid relation
     ([renv_eq]) rather than [functional_extensionality], so [Print
     Assumptions] stays clean — order-insensitivity is *definitional*
     (the carrier is a function; permutation collapses to [renv_eq]),