diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
index f1e93ca3cf..a5ba5d8ec5 100644
--- a/arch/rv32i/src/pmp.rs
+++ b/arch/rv32i/src/pmp.rs
@@ -110,17 +110,21 @@ impl From<mpu::Permissions> for TORUserPMPCFG {
 /// [`NAPOTRegionSpec::napot_addr`] convenience method to retrieve an `pmpaddrX`
 /// CSR value encoding this region's address and length.
 #[derive(Copy, Clone, Debug)]
+// #[flux::refined_by(a: u32)]
 pub struct NAPOTRegionSpec {
     start: *const u8,
+    // #[flux::field({ u32[a] | a > 0 })]
     size: usize,
 }
 
+#[flux::ignore]
 impl NAPOTRegionSpec {
     /// Construct a new [`NAPOTRegionSpec`]
     ///
     /// This method accepts a `start` address and a region length. It returns
     /// `Some(region)` when all constraints specified in the
     /// [`NAPOTRegionSpec`]'s documentation are satisfied, otherwise `None`.
+    #[flux::ignore]
     pub fn new(start: *const u8, size: usize) -> Option<Self> {
         if !size.is_power_of_two() || (start as usize) % size != 0 || size < 8 {
             None
@@ -207,6 +211,9 @@ impl TORRegionSpec {
 ///
 /// Matching the RISC-V spec this checks pmpaddr[i-i] <= y < pmpaddr[i] for TOR
 /// ranges.
+// #[flux::sig(fn() -> usize{v: v < FORTY_TWO})]
+// Other size should be > 0
+#[flux::ignore]
 fn region_overlaps(
     region: &(TORUserPMPCFG, *const u8, *const u8),
     other_start: *const u8,
@@ -234,12 +241,15 @@ fn region_overlaps(
     //
     // This implementation is simple and stupid, and can be optimized. We leave
     // that as an exercise to the compiler.
+
+    let end = region_range.end - 1;
+
     !region_range.is_empty()
         && !other_range.is_empty()
         && (region_range.contains(&other_range.start)
             || region_range.contains(&(other_range.end - 1))
             || other_range.contains(&region_range.start)
-            || other_range.contains(&(region_range.end - 1)))
+            || other_range.contains(&(end)))
 }
 
 /// Print a table of the configured PMP regions, read from  the HW CSRs.
@@ -250,6 +260,7 @@ fn region_overlaps(
 /// the hardware to feature `PHYSICAL_ENTRIES` PMP CSR entries. If these
 /// conditions are not met, calling this function can result in undefinied
 /// behavior (e.g., cause a system trap).
+#[flux::ignore]
 pub unsafe fn format_pmp_entries<const PHYSICAL_ENTRIES: usize>(
     f: &mut fmt::Formatter<'_>,
 ) -> fmt::Result {
@@ -479,6 +490,8 @@ pub trait TORUserPMP<const MAX_REGIONS: usize> {
 }
 
 /// Struct storing userspace memory protection regions for the [`PMPUserMPU`].
+// #[flux::invariant(MAX_REGIONS > 0)]
+// #[flux::invariant(MAX_REGIONS <= 16)]
 pub struct PMPUserMPUConfig<const MAX_REGIONS: usize> {
     /// PMP config identifier, as generated by the issuing PMP implementation.
     id: NonZeroUsize,
@@ -486,6 +499,7 @@ pub struct PMPUserMPUConfig<const MAX_REGIONS: usize> {
     /// written to hardware.
     is_dirty: Cell<bool>,
     /// Array of MPU regions. Each region requires two physical PMP entries.
+    // #[flux::field({ ? | MAX_REGIONS > 0 })]
     regions: [(TORUserPMPCFG, *const u8, *const u8); MAX_REGIONS],
     /// Which region index (into the `regions` array above) is used
     /// for app memory (if it has been configured).
@@ -876,6 +890,7 @@ impl<const MAX_REGIONS: usize, P: TORUserPMP<MAX_REGIONS> + 'static> kernel::pla
 pub mod test {
     use super::{TORUserPMP, TORUserPMPCFG};
 
+    #[allow(dead_code)]
     struct MockTORUserPMP;
     impl<const MPU_REGIONS: usize> TORUserPMP<MPU_REGIONS> for MockTORUserPMP {
         // Don't require any const-assertions in the MockTORUserPMP.