diff --git a/Cargo.toml b/Cargo.toml
index 3f1cae2c06..a3522b0a53 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -93,7 +93,7 @@ members = [
     "libraries/riscv-csr",
     "libraries/tock-cells",
     "libraries/tock-register-interface",
-    "libraries/tickv",
+    "libraries/tickv", "flux_support",
 ]
 exclude = ["tools/"]
 resolver = "2"
diff --git a/arch/cortex-m/Cargo.toml b/arch/cortex-m/Cargo.toml
index e0e547ba30..40c438d700 100644
--- a/arch/cortex-m/Cargo.toml
+++ b/arch/cortex-m/Cargo.toml
@@ -13,3 +13,4 @@ enabled = true
 
 [dependencies]
 kernel = { path = "../../kernel" }
+flux_support = { path = "../../flux_support" }
diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs
index 0e8d6f401b..719db48b52 100644
--- a/arch/cortex-m/src/mpu.rs
+++ b/arch/cortex-m/src/mpu.rs
@@ -16,7 +16,10 @@ use kernel::utilities::math;
 use kernel::utilities::registers::interfaces::{Readable, Writeable};
 use kernel::utilities::registers::{register_bitfields, FieldValue, ReadOnly, ReadWrite};
 use kernel::utilities::StaticRef;
+use flux_support::*;
 
+/*
+#[allow(dead_code)]
 #[flux::sig(fn(x: bool[true]))]
 fn assert(_x: bool) {}
 
@@ -26,6 +29,7 @@ pub fn assume(b: bool) {
         panic!("assume fails")
     }
 }
+*/
 
 // VTOCK-TODO: supplementary proof?
 #[flux::sig(fn(n: u32{n < 32}) -> usize {r: r > 0 })]
@@ -651,9 +655,8 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
         // Region size is the actual size the MPU region will be set to, and is
         // half of the total power of two size we are allocating to the app.
 
-        //assume(memory_size_po2 > 1);
         let mut region_size = memory_size_po2 / 2;
-        //assume(region_size > 0);
+
         // The region should start as close as possible to the start of the
         // unallocated memory.
         let mut region_start = unallocated_memory_start as usize;
@@ -760,6 +763,9 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
         let app_memory_break = app_memory_break as usize;
         let kernel_memory_break = kernel_memory_break as usize;
 
+        assume(app_memory_break > region_start);
+        assume(region_size > 7);
+
         // Out of memory
         if app_memory_break > kernel_memory_break {
             return Err(());
@@ -785,6 +791,7 @@ impl<const MIN_REGION_SIZE: usize> mpu::MPU for MPU<MIN_REGION_SIZE> {
 
         // Get the number of subregions enabled in each of the two MPU regions.
         let num_enabled_subregions0 = cmp::min(num_enabled_subregions, 8);
+        assume(num_enabled_subregions0 >= 8);
         let num_enabled_subregions1 = num_enabled_subregions.saturating_sub(8);
 
         let region0 = CortexMRegion::new(
diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml
index b0b325964d..2bd0aa18de 100644
--- a/kernel/Cargo.toml
+++ b/kernel/Cargo.toml
@@ -15,6 +15,7 @@ enabled = true
 tock-registers = { path = "../libraries/tock-register-interface" }
 tock-cells = { path = "../libraries/tock-cells" }
 tock-tbf = { path = "../libraries/tock-tbf" }
+flux_support = { path = "../flux_support" }
 
 # In general, Tock discourages the use of cargo features. However for certain
 # kernel crate configuration, we have not found reasonable alternatives to
diff --git a/kernel/src/memop.rs b/kernel/src/memop.rs
index 6bdcfb1309..73024d1d78 100644
--- a/kernel/src/memop.rs
+++ b/kernel/src/memop.rs
@@ -7,6 +7,7 @@
 use crate::process::TockProc;
 use crate::syscall::SyscallReturn;
 use crate::ErrorCode;
+use flux_support::*;
 
 /// Handle the `memop` syscall.
 ///
@@ -80,6 +81,7 @@ pub(crate) fn memop(process: &TockProc<'_>, op_type: usize, r1: usize) -> Syscal
             if size == 0 {
                 SyscallReturn::Failure(ErrorCode::FAIL)
             } else {
+                assume(flash_start < u32::MAX / 2 && offset < u32::MAX / 4);
                 SyscallReturn::SuccessU32(flash_start + offset)
             }
         }
@@ -93,6 +95,7 @@ pub(crate) fn memop(process: &TockProc<'_>, op_type: usize, r1: usize) -> Syscal
             if size == 0 {
                 SyscallReturn::Failure(ErrorCode::FAIL)
             } else {
+                assume(flash_start < u32::MAX / 2 && offset < u32::MAX / 4 && size < u32::MAX / 4);
                 SyscallReturn::SuccessU32(flash_start + offset + size)
             }
         }
diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs
index 49e9f8ce4c..785170fe52 100644
--- a/kernel/src/platform/mpu.rs
+++ b/kernel/src/platform/mpu.rs
@@ -6,6 +6,7 @@
 
 use core::cmp;
 use core::fmt::{self, Display};
+ use flux_support::*;
 
 /// User mode access permissions.
 #[derive(Copy, Clone, Debug)]
@@ -312,6 +313,8 @@ impl MPU for () {
         _permissions: Permissions,
         _config: &mut Self::MpuConfig,
     ) -> Option<(*const u8, usize)> {
+        assume(initial_app_memory_size < usize::MAX / 2);
+        assume(initial_kernel_memory_size < usize::MAX / 2);
         let memory_size = cmp::max(
             min_memory_size,
             initial_app_memory_size + initial_kernel_memory_size,
diff --git a/kernel/src/process_checker.rs b/kernel/src/process_checker.rs
index da52f48558..68d6cb288b 100644
--- a/kernel/src/process_checker.rs
+++ b/kernel/src/process_checker.rs
@@ -169,6 +169,37 @@ impl Compress for () {
 pub trait AppIdPolicy: AppUniqueness + Compress {}
 impl<T: AppUniqueness + Compress> AppIdPolicy for T {}
 
+#[allow(dead_code, unused_variables)]
+#[flux::opaque]
+#[flux::trusted]
+pub struct AppIdPolicyProxy<'a> {
+    _inner: &'a dyn AppIdPolicy,
+}
+
+impl<'a> AppIdPolicyProxy<'a> {
+    pub fn to_short_id(&self, _process: &ProcessBinary) -> ShortId { unimplemented!() }
+    pub fn different_identifier(&self, _process_a: &ProcessBinary, _process_b: &ProcessBinary) -> bool {
+        unimplemented!()
+    }
+
+    pub fn different_identifier_process(
+        &self,
+        _process_a: &ProcessBinary,
+        _process_b: &TockProc<'_>,
+    ) -> bool {
+        unimplemented!()
+    }
+
+    pub fn different_identifier_processes(
+        &self,
+        _process_a: &TockProc<'_>,
+        _process_b: &TockProc<'_>,
+    ) -> bool {
+        unimplemented!()
+    }
+}
+
+
 /// Client interface for the outcome of a process credential check.
 pub trait ProcessCheckerMachineClient {
     /// Check is finished, and the check result is in `result`.0
diff --git a/kernel/src/process_loading.rs b/kernel/src/process_loading.rs
index 1a45713bac..a7646f221d 100644
--- a/kernel/src/process_loading.rs
+++ b/kernel/src/process_loading.rs
@@ -15,7 +15,7 @@
 use core::cell::Cell;
 use core::fmt;
 
-use crate::capabilities::ProcessManagementCapability;
+use crate::capabilities::ProcessManagementCap;
 use crate::config;
 use crate::debug;
 use crate::deferred_call::{DeferredCall, DeferredCallClient};
@@ -23,8 +23,8 @@ use crate::kernel::Kernel;
 use crate::platform::chip::Chip;
 use crate::process::{ShortId, TockProc};
 use crate::process_binary::{ProcessBinary, ProcessBinaryError};
-use crate::process_checker::{AppIdPolicy, ProcessCheckError, ProcessCheckerMachine};
-use crate::process_policies::ProcessFaultPolicy;
+use crate::process_checker::{AppIdPolicyProxy, ProcessCheckError, ProcessCheckerMachine};
+use crate::process_policies::ProcessFaultPolicyProxy;
 use crate::process_standard::ProcessStandard;
 use crate::utilities::cells::{MapCell, OptionalCell};
 
@@ -137,8 +137,8 @@ pub fn load_processes<C: Chip>(
     app_flash: &'static [u8],
     app_memory: &'static mut [u8],
     mut procs: &'static mut [Option<TockProc<'_>>],
-    fault_policy: &'static dyn ProcessFaultPolicy,
-    _capability_management: &dyn ProcessManagementCapability,
+    fault_policy: &'static ProcessFaultPolicyProxy,
+    _capability_management: &ProcessManagementCap,
 ) -> Result<(), ProcessLoadError> {
     load_processes_from_flash(
         kernel,
@@ -187,7 +187,7 @@ fn load_processes_from_flash<C: Chip>(
     app_flash: &'static [u8],
     app_memory: &'static mut [u8],
     procs: &mut &'static mut [Option<TockProc<'_>>],
-    fault_policy: &'static dyn ProcessFaultPolicy,
+    fault_policy: &'static ProcessFaultPolicyProxy,
 ) -> Result<(), ProcessLoadError> {
     if config::CONFIG.debug_load_processes {
         debug!(
@@ -348,7 +348,7 @@ fn load_process<C: Chip>(
     app_memory: &'static mut [u8],
     app_id: ShortId,
     index: usize,
-    fault_policy: &'static dyn ProcessFaultPolicy,
+    fault_policy: &'static ProcessFaultPolicyProxy,
 ) -> Result<(&'static mut [u8], Option<TockProc<'static>>), (&'static mut [u8], ProcessLoadError)> {
     if config::CONFIG.debug_load_processes {
         debug!(
@@ -418,6 +418,20 @@ pub trait ProcessLoadingAsyncClient {
     fn process_loading_finished(&self);
 }
 
+#[allow(dead_code, unused_variables)]
+#[flux::opaque]
+#[flux::trusted]
+pub struct ProcessLoadingAsyncClientProxy<'a> {
+    _inner: &'a dyn ProcessLoadingAsyncClient,
+}
+
+impl<'a> ProcessLoadingAsyncClientProxy<'a> {
+    fn process_loaded(&self, _result: Result<(), ProcessLoadError>) {unimplemented!()}
+
+    fn process_loading_finished(&self) {unimplemented!()}
+}
+
+
 /// Asynchronous process loading.
 ///
 /// Machines which implement this trait perform asynchronous process loading and
@@ -428,10 +442,10 @@ pub trait ProcessLoadingAsyncClient {
 pub trait ProcessLoadingAsync<'a> {
     /// Set the client to receive callbacks about process loading and when
     /// process loading has finished.
-    fn set_client(&self, client: &'a dyn ProcessLoadingAsyncClient);
+    fn set_client(&self, client: &'a ProcessLoadingAsyncClientProxy<'a>);
 
     /// Set the credential checking policy for the loader.
-    fn set_policy(&self, policy: &'a dyn AppIdPolicy);
+    fn set_policy(&self, policy: &'a AppIdPolicyProxy);
 
     /// Start the process loading operation.
     fn start(&self);
@@ -454,7 +468,7 @@ enum SequentialProcessLoaderMachineState {
 /// the checker to decide whether the process has sufficient credentials to run.
 pub struct SequentialProcessLoaderMachine<'a, C: Chip + 'static> {
     /// Client to notify as processes are loaded and process loading finishes.
-    client: OptionalCell<&'a dyn ProcessLoadingAsyncClient>,
+    client: OptionalCell<&'a ProcessLoadingAsyncClientProxy<'a>>,
     /// Machine to use to check process credentials.
     checker: &'static ProcessCheckerMachine,
     /// Array of stored process references for loaded processes.
@@ -472,9 +486,9 @@ pub struct SequentialProcessLoaderMachine<'a, C: Chip + 'static> {
     /// Reference to the Chip object for creating Processes.
     chip: &'static C,
     /// The policy to use when determining ShortIds and process uniqueness.
-    policy: OptionalCell<&'a dyn AppIdPolicy>,
+    policy: OptionalCell<&'a AppIdPolicyProxy<'a>>,
     /// The fault policy to assign to each created Process.
-    fault_policy: &'static dyn ProcessFaultPolicy,
+    fault_policy: &'static ProcessFaultPolicyProxy<'static>,
     /// Current mode of the loading machine.
     state: OptionalCell<SequentialProcessLoaderMachineState>,
 }
@@ -492,9 +506,9 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
         chip: &'static C,
         flash: &'static [u8],
         app_memory: &'static mut [u8],
-        fault_policy: &'static dyn ProcessFaultPolicy,
-        policy: &'static dyn AppIdPolicy,
-        _capability_management: &dyn ProcessManagementCapability,
+        fault_policy: &'static ProcessFaultPolicyProxy<'static>,
+        policy: &'static AppIdPolicyProxy,
+        _capability_management: &ProcessManagementCap,
     ) -> Self {
         Self {
             deferred_call: DeferredCall::new(),
@@ -855,11 +869,11 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
 }
 
 impl<'a, C: Chip> ProcessLoadingAsync<'a> for SequentialProcessLoaderMachine<'a, C> {
-    fn set_client(&self, client: &'a dyn ProcessLoadingAsyncClient) {
+    fn set_client(&self, client: &'a ProcessLoadingAsyncClientProxy<'a>) {
         self.client.set(client);
     }
 
-    fn set_policy(&self, policy: &'a dyn AppIdPolicy) {
+    fn set_policy(&self, policy: &'a AppIdPolicyProxy) {
         self.policy.replace(policy);
     }
 
diff --git a/kernel/src/process_policies.rs b/kernel/src/process_policies.rs
index 34542b1844..713a309af4 100644
--- a/kernel/src/process_policies.rs
+++ b/kernel/src/process_policies.rs
@@ -21,6 +21,18 @@ pub trait ProcessFaultPolicy {
     fn action(&self, process: &TockProc<'_>) -> process::FaultAction;
 }
 
+#[allow(dead_code, unused_variables)]
+#[flux::opaque]
+#[flux::trusted]
+pub struct ProcessFaultPolicyProxy<'a> {
+    _inner: &'a dyn ProcessFaultPolicy,
+}
+
+impl<'a> ProcessFaultPolicyProxy<'a> {
+    pub fn action(&self, _process: &TockProc<'_>) -> process::FaultAction {unimplemented!()}
+}
+
+
 /// Simply panic the entire board if a process faults.
 pub struct PanicFaultPolicy {}
 
diff --git a/kernel/src/process_standard.rs b/kernel/src/process_standard.rs
index ce42b17c0f..09f1060fff 100644
--- a/kernel/src/process_standard.rs
+++ b/kernel/src/process_standard.rs
@@ -29,12 +29,13 @@ use crate::process::{Error, FunctionCall, FunctionCallSource, Process, State, Ta
 use crate::process::{FaultAction, ProcessCustomGrantIdentifier, ProcessId};
 use crate::process::{ProcessAddresses, ProcessSizes, ShortId};
 use crate::process_loading::ProcessLoadError;
-use crate::process_policies::ProcessFaultPolicy;
 use crate::processbuffer::{ReadOnlyProcessBuffer, ReadWriteProcessBuffer};
 use crate::storage_permissions;
 use crate::syscall::{self, Syscall, SyscallReturn, UserspaceKernelBoundary};
 use crate::upcall::UpcallId;
 use crate::utilities::cells::{MapCell, NumericCellExt, OptionalCell};
+use crate::process_policies::ProcessFaultPolicyProxy;
+
 
 use tock_tbf::types::CommandPermissions;
 
@@ -203,7 +204,7 @@ pub struct ProcessStandard<'a, C: 'static + Chip> {
     state: Cell<State>,
 
     /// How to respond if this process faults.
-    fault_policy: &'a dyn ProcessFaultPolicy,
+    fault_policy: &'a ProcessFaultPolicyProxy<'a>,
 
     /// Configuration data for the MPU
     mpu_config: MapCell<<<C as Chip>::MPU as MPU>::MpuConfig>,
@@ -1162,7 +1163,7 @@ impl<C: Chip> Process for ProcessStandard<'_, C> {
             process_control_block: Self::PROCESS_STRUCT_OFFSET,
         }
     }
-
+    #[flux::ignore]
     fn print_full_process(&self, writer: &mut dyn Write) {
         if !config::CONFIG.debug_panics {
             return;
@@ -1281,7 +1282,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
         chip: &'static C,
         pb: ProcessBinary,
         remaining_memory: &'a mut [u8],
-        fault_policy: &'static dyn ProcessFaultPolicy,
+        fault_policy: &'static ProcessFaultPolicyProxy,
         app_id: ShortId,
         index: usize,
     ) -> Result<(Option<TockProc<'static>>, &'a mut [u8]), (ProcessLoadError, &'a mut [u8])> {
diff --git a/kernel/src/utilities/math.rs b/kernel/src/utilities/math.rs
index 32e5339a9a..7a64e87682 100644
--- a/kernel/src/utilities/math.rs
+++ b/kernel/src/utilities/math.rs
@@ -116,6 +116,7 @@ pub fn log_base_two_u64(num: u64) -> u32 {
 const EXPONENT_MASK: u32 = 0b01111111_10000000_00000000_00000000;
 const EXPONENT_BIAS: u32 = 127;
 
+#[flux::ignore]
 pub fn abs(n: f32) -> f32 {
     f32::from_bits(n.to_bits() & 0x7FFF_FFFF)
 }
@@ -124,10 +125,12 @@ fn extract_exponent_bits(x: f32) -> u32 {
     (x.to_bits() & EXPONENT_MASK).overflowing_shr(23).0
 }
 
+#[flux::ignore]
 fn extract_exponent_value(x: f32) -> i32 {
     (extract_exponent_bits(x) as i32) - EXPONENT_BIAS as i32
 }
 
+#[flux::ignore]
 fn ln_1to2_series_approximation(x: f32) -> f32 {
     // idea from https://stackoverflow.com/a/44232045/
     // modified to not be restricted to int range and only values of x above 1.0.
@@ -165,6 +168,7 @@ fn ln_1to2_series_approximation(x: f32) -> f32 {
     }
 }
 
+#[flux::ignore]
 pub fn log10(x: f32) -> f32 {
     //using change of base log10(x) = ln(x)/ln(10)
     let ln10_recip = f32::consts::LOG10_E;