diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail
index 8b5bf2bd8..e7083c014 100644
--- a/model/riscv_extensions.sail
+++ b/model/riscv_extensions.sail
@@ -6,6 +6,17 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+// Privileged and unprivileged spec versions. The versioning system for specifications
+// is unclear so we just use the commit date. This also allows versioning for specs changes
+// that are between releases. If there was an official release for this day (for example
+// 20240411) then this is the commit of that release. Otherwise it is for the *last*
+// commit on the given day.
+type SpecVersion = range(20000000, 21000000)
+
+// TODO: Replace with 'config ...priv_version' or similar when the config system is available.
+let configPrivVersion : SpecVersion = 20240411
+let configUnprivVersion : SpecVersion = 20240411
+
 scattered enum extension
 
 // Note, these are sorted according to the canonical ordering vaguely described
diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail
index ce5b19d7a..84ed05a9a 100644
--- a/model/riscv_vmem_pte.sail
+++ b/model/riscv_vmem_pte.sail
@@ -77,18 +77,22 @@ function clause extensionEnabled(Ext_Svpbmt) = false
 function pte_is_invalid(pte_flags : PTE_Flags, pte_ext : PTE_Ext) -> bool =
     pte_flags[V] == 0b0
   | (pte_flags[W] == 0b1 & pte_flags[R] == 0b0)
-  // Note, the following requirements depend on the privileged spec version.
-  // Early versions do not require this check. This will need to be behind
-  // a flag when the Sail model allows specifying the spec version.
-  | (pte_ext[N] != 0b0 & not(extensionEnabled(Ext_Svnapot)))
-  | (pte_ext[PBMT] != zeros() & not(extensionEnabled(Ext_Svpbmt)))
-  | pte_ext[reserved] != zeros()
+  // Since spec commit 31bc179b214fc0374075ea9284aa939b8341b843, reserved bits must be zero.
+  | configPrivVersion >= 20211101 & (
+    // All bits are currently reserved for non-leaf PTEs.
+      pte_is_ptr(pte_flags) & pte_ext.bits != zeros()
+    // N/PBMT are reserved if not implemented.
+    | pte_ext[N]        != zeros() & not(extensionEnabled(Ext_Svnapot))
+    | pte_ext[PBMT]     != zeros() & not(extensionEnabled(Ext_Svpbmt))
+    // Other bits are reserved even for leaf PTEs.
+    | pte_ext[reserved] != zeros()
+  )
 
 // ----------------
 // Check access permissions in PTE
 
 // For (non-standard) extensions: this function gets the extension-available bits
-// of the PTE in extPte, and the accumulated information of the page-table-walk
+// of the PTE in PTE_Ext, and the accumulated information of the page-table-walk
 // in ext_ptw. It should return the updated ext_ptw in both success and failure cases.
 
 union PTE_Check = {