diff --git a/kernel/src/hil/can.rs b/kernel/src/hil/can.rs
index 9425299afe..1d38b375d8 100644
--- a/kernel/src/hil/can.rs
+++ b/kernel/src/hil/can.rs
@@ -228,7 +228,7 @@ pub trait StandardBitTiming {
 /// is inspired by the Zephyr CAN driver available at
 /// `<https://github.com/zephyrproject-rtos/zephyr/tree/main/drivers/can>`
 impl<T: Configure> StandardBitTiming for T {
-    // #[flux_rs::trusted] // VTOCK: error jumping to join point
+    #[flux_rs::trusted] // VTOCK: error jumping to join point
     fn bit_timing_for_bitrate(clock_rate: u32, bitrate: u32) -> Result<BitTiming, ErrorCode> {
         fn calc_sample_point_err(
             sp: u32,
diff --git a/kernel/src/process_loading.rs b/kernel/src/process_loading.rs
index 2d8106522a..192b881acc 100644
--- a/kernel/src/process_loading.rs
+++ b/kernel/src/process_loading.rs
@@ -589,7 +589,6 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
     ///
     /// Returns the process binary object or an error if a valid process
     /// binary could not be extracted.
-    #[flux_rs::trusted] // error jumping to join point
     fn discover_process_binary(&self) -> Result<ProcessBinary, ProcessBinaryError> {
         let flash = self.flash.get();
         assume(flash.len() > 0); // Need to guarantee &[u8] inside Cell is not 0
diff --git a/kernel/src/process_standard.rs b/kernel/src/process_standard.rs
index dff890a5e6..e622047488 100644
--- a/kernel/src/process_standard.rs
+++ b/kernel/src/process_standard.rs
@@ -318,7 +318,6 @@ impl<C: Chip> Process for ProcessStandard<'_, C> {
             || self.state.get() == State::Running
     }
 
-    #[flux_rs::trusted] // incompatible types
     fn remove_pending_upcalls(&self, upcall_id: UpcallId) {
         self.tasks.map(|tasks| {
             let count_before = tasks.len();
@@ -454,7 +453,6 @@ impl<C: Chip> Process for ProcessStandard<'_, C> {
         // want to reclaim the process resources.
     }
 
-    #[flux_rs::trusted] // incompatible types
     fn terminate(&self, completion_code: Option<u32>) {
         // A process can be terminated if it is running or in the `Faulted`
         // state. Otherwise, you cannot terminate it and this method return
@@ -1359,7 +1357,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     const PROCESS_STRUCT_OFFSET: usize = mem::size_of::<ProcessStandard<C>>();
 
     /// Create a `ProcessStandard` object based on the found `ProcessBinary`.
-    #[flux_rs::trusted] // ICE: Cannot move out of non-strong reference
+    #[flux_rs::trusted] // ICE: UnsolvedEvar
     pub(crate) unsafe fn create<'a>(
         kernel: &'static Kernel,
         chip: &'static C,
diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs
index 3020726d50..b0551848a2 100644
--- a/kernel/src/processbuffer.rs
+++ b/kernel/src/processbuffer.rs
@@ -762,7 +762,8 @@ impl ReadableProcessSlice {
     ///
     /// The length of `self` must be the same as `dest`. Subslicing
     /// can be used to obtain a slice of matching length.
-    #[flux_rs::trusted] // ICE" expected array or slice type
+    #[flux_rs::trusted] // Need spec for enumerate
+    #[flux_rs::sig(fn (self: &Self, dest: &strg [u8]) -> Result<(), ErrorCode> ensures dest: [u8] )]
     pub fn copy_to_slice_or_err(&self, dest: &mut [u8]) -> Result<(), ErrorCode> {
         // Method implemetation adopted from the
         // core::slice::copy_from_slice method implementation: