diff --git a/capsules/core/Cargo.toml b/capsules/core/Cargo.toml
index 559c3f9d61..56aa411949 100644
--- a/capsules/core/Cargo.toml
+++ b/capsules/core/Cargo.toml
@@ -12,10 +12,12 @@ edition.workspace = true
 kernel = { path = "../../kernel" }
 enum_primitive = { path = "../../libraries/enum_primitive" }
 tickv = { path = "../../libraries/tickv" }
+flux-rs = { git  = "https://github.com/flux-rs/flux.git" }
 
 [package.metadata.flux]
 enabled = true
 check_overflow = "lazy"
+no_panic = true
 include = [ "src/button.rs", "src/led.rs", "src/console.rs", "src/alarm.rs", "src/spi_peripheral.rs", "src/stream.rs"  ]
 
 [lints]
diff --git a/capsules/core/src/alarm.rs b/capsules/core/src/alarm.rs
index cbab6e5234..780088ef2a 100644
--- a/capsules/core/src/alarm.rs
+++ b/capsules/core/src/alarm.rs
@@ -9,6 +9,7 @@ use kernel::grant::{AllowRoCount, AllowRwCount, Grant, UpcallCount};
 use kernel::hil::time::{self, Alarm, Ticks};
 use kernel::syscall::{CommandReturn, SyscallDriver};
 use kernel::{ErrorCode, ProcessId};
+use kernel::process;
 
 /// Syscall driver number.
 use crate::driver;
@@ -76,6 +77,8 @@ impl<'a, A: Alarm<'a>> AlarmDriver<'a, A> {
     /// To stop iteration on any expired [`Expiration`], its callback can return
     /// `Some(R)`. Then this function will return `Err(Expiration, UD, R)`.
     /// This avoids consuming the entire iterator.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted] // Andrew note: trusted because of closure usage
     fn earliest_alarm<UD, R, F: FnOnce(Expiration<A::Ticks>, &UD) -> Option<R>>(
         now: A::Ticks,
         expirations: impl Iterator<Item = (Expiration<A::Ticks>, UD, F)>,
@@ -150,6 +153,8 @@ impl<'a, A: Alarm<'a>> AlarmDriver<'a, A> {
     /// - invoke upcalls for all expired app alarms, resetting them afterwards,
     /// - re-arming the alarm for the next earliest [`Expiration`], or
     /// - disarming the alarm if no unexpired [`Expiration`] is found.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted] // Andrew note: The `unreachable!()` here needs to be a refinement
     fn process_rearm_or_callback(&self) {
         // Ask the clock about a current reference once. This can incur a
         // volatile read, and this may not be optimized if done in a loop:
@@ -501,7 +506,7 @@ impl<'a, A: Alarm<'a>> SyscallDriver for AlarmDriver<'a, A> {
                 }
             })
             .map_or_else(
-                |err| CommandReturn::failure(err.into()),
+                |err: process::Error| CommandReturn::failure(err.into()),
                 |(retval, rearm_timer)| {
                     if rearm_timer {
                         self.process_rearm_or_callback();
diff --git a/flux_support/src/extern_specs/cell.rs b/flux_support/src/extern_specs/cell.rs
new file mode 100644
index 0000000000..995dbcb63c
--- /dev/null
+++ b/flux_support/src/extern_specs/cell.rs
@@ -0,0 +1,28 @@
+use core::cell::Cell;
+
+#[flux_rs::extern_spec(core::cell)]
+struct Cell<T: ?Sized>;
+
+#[flux_rs::extern_spec(core::cell)]
+impl<T: Copy> Cell<T> {
+    #[flux_rs::no_panic]
+    fn get(&self) -> T;
+}
+
+#[flux_rs::extern_spec(core::cell)]
+impl<T> Cell<T> {
+    #[flux_rs::no_panic]
+    fn new(value: T) -> Cell<T>;
+
+    #[flux_rs::no_panic]
+    fn set(&self, value: T);
+
+    #[flux_rs::no_panic]
+    fn replace(&self, val: T) -> T;
+}
+
+#[flux_rs::extern_spec(core::cell)]
+impl<T: Default> Cell<T> {
+    #[flux_rs::no_panic]
+    fn take(&self) -> T;
+}
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/cmp.rs b/flux_support/src/extern_specs/cmp.rs
new file mode 100644
index 0000000000..0ad6166780
--- /dev/null
+++ b/flux_support/src/extern_specs/cmp.rs
@@ -0,0 +1,7 @@
+#[flux_rs::extern_spec(core::cmp)]
+#[flux_rs::no_panic]
+fn min<T: Ord>(v1: T, v2: T) -> T;
+
+#[flux_rs::extern_spec(core::cmp)]
+#[flux_rs::no_panic]
+fn max<T: Ord>(v1: T, v2: T) -> T;
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/default.rs b/flux_support/src/extern_specs/default.rs
new file mode 100644
index 0000000000..49179fd666
--- /dev/null
+++ b/flux_support/src/extern_specs/default.rs
@@ -0,0 +1,5 @@
+#[flux_rs::extern_spec(core::default)]
+trait Default {
+    #[flux_rs::no_panic]
+    fn default() -> Self;
+}
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/fmt.rs b/flux_support/src/extern_specs/fmt.rs
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/flux_support/src/extern_specs/from.rs b/flux_support/src/extern_specs/from.rs
new file mode 100644
index 0000000000..70beec2b10
--- /dev/null
+++ b/flux_support/src/extern_specs/from.rs
@@ -0,0 +1,18 @@
+#[flux_rs::extern_spec(core::convert)]
+trait From<T>: Sized {
+    #[flux_rs::no_panic]
+    fn from(value: T) -> Self;
+}
+
+#[flux_rs::extern_spec(core::convert)]
+trait Into<T>: Sized {
+    #[flux_rs::no_panic]
+    fn into(self) -> T;
+}
+
+
+#[flux_rs::extern_spec(core::convert)]
+impl<T, U: From<T>> Into<U> for T {
+    #[flux_rs::no_panic]
+    fn into(self) -> U;
+}
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/func.rs b/flux_support/src/extern_specs/func.rs
new file mode 100644
index 0000000000..2d9bb3f1e6
--- /dev/null
+++ b/flux_support/src/extern_specs/func.rs
@@ -0,0 +1,5 @@
+// #[flux_rs::extern_spec]
+// trait FnOnce<Args: Tuple> {
+//     #[flux_rs::no_panic]
+//     fn call_once(&self) -> Self::Output;
+// }
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs
index 8d8dfa6f84..6193dd5d3a 100644
--- a/flux_support/src/extern_specs/iter.rs
+++ b/flux_support/src/extern_specs/iter.rs
@@ -1,11 +1,32 @@
 #![allow(unused)]
 use crate::assert;
-use core::slice::Iter;
+use core::iter::Enumerate;
+use core::iter::FilterMap;
+use core::iter::IntoIterator;
 
 #[flux_rs::extern_spec(core::slice)]
 #[flux_rs::refined_by(idx: int, len: int)]
 struct Iter<'a, T>;
 
+#[flux_rs::extern_spec]
+trait FromIterator<A> {}
+
+#[flux_rs::extern_spec(core::iter)]
+trait IntoIterator {
+    #[flux_rs::spec(fn(self: Self) -> Self::IntoIter)]
+    #[flux_rs::no_panic]
+    fn into_iter(self) -> Self::IntoIter
+    where
+        Self: Sized;
+}
+
+#[flux_rs::extern_spec(core::ops)]
+impl<I: Iterator> IntoIterator for I {
+    #[flux_rs::spec(fn(self: I[@s]) -> I[s])]
+    #[flux_rs::no_panic]
+    fn into_iter(self) -> I;
+}
+
 // #[flux_rs::extern_spec(std::iter)]
 // #[flux_rs::refined_by(idx: int, inner: I)]
 // struct Enumerate<I>;
@@ -13,15 +34,64 @@ struct Iter<'a, T>;
 // #[flux_rs::extern_spec(std::iter)]
 // #[flux_rs::assoc(fn done(self: Self) -> bool )]
 // #[flux_rs::assoc(fn step(self: Self, other: Self) -> bool )]
-// trait Iterator {
-//     #[flux_rs::sig(fn(self: &strg Self[@curr_s]) -> Option<Self::Item>[!<Self as Iterator>::done(curr_s)] ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)})]
-//     fn next(&mut self) -> Option<Self::Item>;
-
-//     #[flux_rs::sig(fn(Self[@s]) -> Enumerate<Self>[0, s])]
-//     fn enumerate(self) -> Enumerate<Self>
-//     where
-//         Self: Sized;
-// }
+
+#[flux_rs::extern_spec(core::iter)]
+trait Iterator {
+    #[flux_rs::no_panic]
+    fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>
+    where
+        Self: Sized,
+        F: FnMut(Self::Item) -> Option<B>;
+
+    #[flux_rs::no_panic]
+    fn find_map<B, F>(&mut self, f: F) -> Option<B>
+    where
+        Self: Sized,
+        F: FnMut(Self::Item) -> Option<B>;
+
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<Self::Item>;
+
+    #[flux_rs::no_panic]
+    fn enumerate(self) -> Enumerate<Self>
+    where
+        Self: Sized;
+
+    #[flux_rs::no_panic]
+    fn rev(self) -> Rev<Self>
+    where
+        Self: Sized + DoubleEndedIterator;
+
+    #[flux_rs::no_panic]
+    fn take(self, n: usize) -> Take<Self>
+    where
+        Self: Sized;
+
+    #[flux_rs::no_panic]
+    fn zip<U>(self, other: U) -> Zip<Self, U::IntoIter>
+    where
+        Self: Sized,
+        U: IntoIterator;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+struct Enumerate<I>;
+
+#[flux_rs::extern_spec(core::iter)]
+impl<I: Iterator> Iterator for Enumerate<I> {
+    // Andrew note: This indeed can panic!
+    // Don't merge until we create a refinement for this so that
+    // we can't call it unless we're sure it won't panic.
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<(usize, I::Item)>;
+}
+
+#[flux_rs::extern_spec(core::iter)]
+impl<A: Iterator, B: Iterator> Iterator for Zip<A, B> {
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<<Zip<A, B> as Iterator>::Item>;
+}
+
 
 // #[flux_rs::extern_spec(std::slice)]
 // #[flux_rs::assoc(fn done(x: Iter<T>) -> bool { x.idx >= x.len })]
diff --git a/flux_support/src/extern_specs/mem.rs b/flux_support/src/extern_specs/mem.rs
index 6479a63993..d2aab51e05 100644
--- a/flux_support/src/extern_specs/mem.rs
+++ b/flux_support/src/extern_specs/mem.rs
@@ -2,4 +2,11 @@
 // https://doc.rust-lang.org/reference/type-layout.html
 #[flux_rs::extern_spec(core::mem)]
 #[flux_rs::sig(fn<T>() -> usize{align: align > 0})]
+#[flux_rs::no_panic]
 fn align_of<T>() -> usize;
+
+
+
+#[flux_rs::extern_spec(core::mem)]
+#[flux_rs::no_panic]
+fn size_of<T>() -> usize;
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs
index 568e0aff94..64e71694f0 100644
--- a/flux_support/src/extern_specs/mod.rs
+++ b/flux_support/src/extern_specs/mod.rs
@@ -1,9 +1,16 @@
+mod cell;
+mod cmp;
+mod default;
+mod func;
+mod fmt;
+mod from;
 mod iter;
 mod mem;
 mod non_null;
 mod num;
 mod option;
 mod partial_cmp;
+mod ptr;
 mod range;
 mod result;
-mod slice;
+mod slice;
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/num.rs b/flux_support/src/extern_specs/num.rs
index 14ad22ac5e..af199dcd44 100644
--- a/flux_support/src/extern_specs/num.rs
+++ b/flux_support/src/extern_specs/num.rs
@@ -9,6 +9,12 @@ impl u32 {
 
     #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && (num != 0 =>r <= 31) })]
     fn trailing_zeros(self) -> u32;
+
+    #[flux_rs::no_panic]
+    fn saturating_sub(self, rhs: u32) -> u32;
+
+    #[flux_rs::no_panic]
+    fn from_be_bytes(bytes: [u8; 4]) -> u32;
 }
 
 #[flux_rs::extern_spec]
diff --git a/flux_support/src/extern_specs/option.rs b/flux_support/src/extern_specs/option.rs
index ae070d769f..6121679d27 100644
--- a/flux_support/src/extern_specs/option.rs
+++ b/flux_support/src/extern_specs/option.rs
@@ -10,8 +10,41 @@ enum Option<T> {
 #[flux_rs::extern_spec]
 impl<T> Option<T> {
     #[sig(fn(&Option<T>[@b]) -> bool[b])]
+    #[flux_rs::no_panic]
     const fn is_some(&self) -> bool;
 
     #[sig(fn(&Option<T>[@b]) -> bool[!b])]
+    #[flux_rs::no_panic]
     const fn is_none(&self) -> bool;
+
+    #[flux_rs::no_panic]
+    fn map_or<U, F>(self, default: U, f: F) -> U
+    where
+        F: FnOnce(T) -> U;
+
+
+    #[flux_rs::no_panic]
+    fn map<U, F>(self, op: F) -> Option<U>
+    where
+        F: FnOnce(T) -> U;
+
+    #[flux_rs::no_panic]
+    fn inspect<F>(self, op: F) -> Self
+    where
+        F: FnOnce(&T);
+
+    #[flux_rs::no_panic]
+    fn unwrap_or_default(self) -> T
+    where
+        T: Default;
+
+    #[flux_rs::no_panic]
+    fn map_or_else<U, D, F>(self, default: D, f: F) -> U
+    where
+        // Andrew note: why does this not match up with source?
+        D: FnOnce() -> U,
+        F: FnOnce(T) -> U;
+
+    #[flux_rs::no_panic]
+    fn ok_or<E>(self, err: E) -> Result<T, E>;
 }
diff --git a/flux_support/src/extern_specs/partial_cmp.rs b/flux_support/src/extern_specs/partial_cmp.rs
index 1dc6d0d1cd..62b57ac717 100644
--- a/flux_support/src/extern_specs/partial_cmp.rs
+++ b/flux_support/src/extern_specs/partial_cmp.rs
@@ -2,10 +2,24 @@
 
 use core::cmp::PartialOrd;
 
-// #[flux_rs::extern_spec(core::cmp)]
-// #[flux_rs::assoc(fn lt(this: Self, other: Self) -> bool)]
-// #[flux_rs::assoc(fn le(this: Self, other: Self) -> bool)]
-// trait PartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
-//     fn lt(&self, other: &Rhs) -> bool;
-//     fn le(&self, other: &Rhs) -> bool;
-// }
+#[flux_rs::extern_spec(core::cmp)]
+trait Ord {
+    #[flux_rs::no_panic]
+    fn min(self, other: Self) -> Self
+    where
+        Self: Sized;
+}
+
+#[flux_rs::extern_spec(core::cmp)]
+trait PartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
+    #[flux_rs::no_panic]
+    fn lt(&self, other: &Rhs) -> bool;
+    fn le(&self, other: &Rhs) -> bool;
+}
+
+
+#[flux_rs::extern_spec(core::cmp)]
+trait PartialEq<Rhs: ?Sized = Self> {
+    #[flux_rs::no_panic]
+    fn eq(&self, other: &Rhs) -> bool;
+}
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/ptr.rs b/flux_support/src/extern_specs/ptr.rs
new file mode 100644
index 0000000000..fa171a86bd
--- /dev/null
+++ b/flux_support/src/extern_specs/ptr.rs
@@ -0,0 +1,15 @@
+use core::marker::PointeeSized;
+
+#[flux_rs::extern_spec(core::ptr)]
+impl<T: Sized> NonNull<T> {
+    #[flux_rs::no_panic]
+    fn as_ptr(self) -> *mut T;
+
+    #[flux_rs::no_panic]
+    fn cast<U>(self) -> NonNull<U>;
+}
+
+#[flux_rs::extern_spec(core::ptr)]
+#[flux_rs::no_panic]
+fn null_mut<T: PointeeSized + Thin>() -> *mut T;
+
diff --git a/flux_support/src/extern_specs/range.rs b/flux_support/src/extern_specs/range.rs
index 1902df310c..90f10c685b 100644
--- a/flux_support/src/extern_specs/range.rs
+++ b/flux_support/src/extern_specs/range.rs
@@ -1,7 +1,10 @@
 #![allow(unused)]
 
 use core::ops::Bound;
+use core::ops;
 use core::ops::{Range, RangeBounds};
+use core::iter::Step;
+
 
 #[flux_rs::extern_spec]
 #[flux_rs::refined_by(included: bool, unbounded: bool)]
@@ -54,6 +57,16 @@ trait RangeBounds<T> {
     // }
 }
 
+
+#[flux_rs::extern_spec(core::iter)]
+trait Step {}
+
+#[flux_rs::extern_spec(core::ops)]
+impl<A: core::iter::Step> Iterator for ops::Range<A> {
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<A>;
+}
+
 #[flux_rs::extern_spec(core::ops)]
 #[flux_rs::assoc(fn start(self: Range<T>) -> T { self.end })]
 #[flux_rs::assoc(fn end(self: Range<T>) -> T { self.end })]
diff --git a/flux_support/src/extern_specs/result.rs b/flux_support/src/extern_specs/result.rs
index 77fae5ae98..32dc8612b8 100644
--- a/flux_support/src/extern_specs/result.rs
+++ b/flux_support/src/extern_specs/result.rs
@@ -12,6 +12,58 @@ impl<T, E> Result<T, E> {
     #[sig(fn(&Result<T,E>[@b]) -> bool[b])]
     const fn is_ok(&self) -> bool;
 
+    #[flux_rs::no_panic]
     #[sig(fn(&Result<T,E>[@b]) -> bool[!b])]
     const fn is_err(&self) -> bool;
+
+    #[flux_rs::no_panic]
+    fn and_then<U, F>(self, op: F) -> Result<U, E>
+    where
+        F: FnOnce(T) -> Result<U, E>;
+
+    #[flux_rs::no_panic]
+    fn map_err<F, O>(self, op: O) -> Result<T, F>
+    where
+        O: FnOnce(E) -> F;
+    
+    #[flux_rs::no_panic]
+    fn map_or<U, F>(self, default: U, f: F) -> U
+    where
+        F: FnOnce(T) -> U;
+
+    #[flux_rs::no_panic]
+    fn map_or_else<U, D, F>(self, default: D, f: F) -> U
+    where
+        D: FnOnce(E) -> U,
+        F: FnOnce(T) -> U;
+    
+    #[flux_rs::no_panic]
+    fn ok(self) -> Option<T>;
+
+    #[flux_rs::no_panic]
+    fn unwrap_or(self, default: T) -> T;
+
+    #[flux_rs::no_panic]
+    fn unwrap_or_default(self) -> T
+    where
+        T: Default;
+
+    #[flux_rs::no_panic]
+    fn unwrap_or_else<F>(self, op: F) -> T
+    where
+        F: FnOnce(E) -> T;
+
+
 }
+
+#[flux_rs::extern_spec(core::ops)]
+impl<T, E> Try for Result<T, E> {
+    #[flux_rs::no_panic]
+    fn branch(self) -> ControlFlow<<Result<T, E> as core::ops::Try>::Residual, <Result<T, E> as core::ops::Try>::Output>;
+}
+
+#[flux_rs::extern_spec(core::ops)]
+impl<T, E, F: From<E>> FromResidual<Result<core::convert::Infallible, E>> for Result<T, F> {
+    #[flux_rs::no_panic]
+    fn from_residual(residual: Result<core::convert::Infallible, E>) -> Self;
+}
\ No newline at end of file
diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs
index 04c7a9b2a5..f9d2cb3ff4 100644
--- a/flux_support/src/extern_specs/slice.rs
+++ b/flux_support/src/extern_specs/slice.rs
@@ -15,12 +15,37 @@ use core::slice::{self, Iter, SliceIndex};
 
 #[flux_rs::extern_spec]
 impl<T> [T] {
+    #[flux_rs::no_panic]
     #[flux_rs::sig(fn(&[T][@len]) -> usize[len])]
     fn len(v: &[T]) -> usize;
 
+    #[flux_rs::no_panic]
     #[flux_rs::sig(fn(&[T][@len]) -> Iter<T>[0, len])]
     fn iter(v: &[T]) -> Iter<'_, T>;
 
     // #[flux_rs::sig(fn(&[T][@len], I[@idx]) -> Option<_>[<I as SliceIndex<[T]>>::in_bounds(idx, len)])]
-    // fn get(&self, index: I) -> Option<&<I as SliceIndex<[T]>>::Output>;
+    #[flux_rs::no_panic]
+    fn get<I: core::slice::SliceIndex<[T]>>(&self, index: I) -> Option<&<I as SliceIndex<[T]>>::Output>;
+
+    #[flux_rs::no_panic]
+    fn copy_from_slice(&mut self, src: &[T]) where
+        T: Copy;
+}
+
+#[flux_rs::extern_spec(core::slice)]
+impl<'a, T> Iterator for Iter<'a, T> {
+    #[flux_rs::no_panic]
+    fn next(&mut self) -> Option<&'a T>;
+}
+
+#[flux_rs::extern_spec]
+impl<T, I: core::slice::SliceIndex<[T]>> core::ops::Index<I> for [T] {
+    #[flux_rs::no_panic]
+    fn index(&self, index: I) -> &I::Output;
 }
+
+#[flux_rs::extern_spec]
+impl<T, I: core::slice::SliceIndex<[T]>> core::ops::IndexMut<I> for [T] {
+    #[flux_rs::no_panic]
+    fn index_mut(&mut self, index: I) -> &mut I::Output;
+}
\ No newline at end of file
diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs
index 6aa9e5ceed..06f8d45395 100644
--- a/flux_support/src/lib.rs
+++ b/flux_support/src/lib.rs
@@ -1,4 +1,8 @@
 #![no_std]
+#![cfg_attr(flux, feature(step_trait))]
+#![feature(try_trait_v2)]
+#![feature(sized_hierarchy)]
+#![feature(ptr_metadata)]
 
 mod extern_specs;
 mod flux_arr;
diff --git a/kernel/src/errorcode.rs b/kernel/src/errorcode.rs
index 887140617b..0ff9602364 100644
--- a/kernel/src/errorcode.rs
+++ b/kernel/src/errorcode.rs
@@ -117,6 +117,7 @@ impl From<ErrorCode> for Result<(), ErrorCode> {
 /// is that [`ErrorCode`], which only expresses errors, is assigned fixed
 /// values, but does not use value 0 by convention. This allows us to use 0 as
 /// success in StatusCode.
+#[flux_rs::no_panic]
 pub fn into_statuscode(r: Result<(), ErrorCode>) -> usize {
     match r {
         Ok(()) => 0,
diff --git a/kernel/src/grant.rs b/kernel/src/grant.rs
index d086ef6e8f..2f759a4b1d 100644
--- a/kernel/src/grant.rs
+++ b/kernel/src/grant.rs
@@ -310,6 +310,12 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> {
     /// not be any other `EnteredGrantKernelManagedLayout` for
     /// the given `base_ptr` at the same time, otherwise multiple mutable
     /// references to the same upcall/allow slices could be created.
+    #[flux_rs::no_panic]
+    // Andrew note: this is here because marking this as _not_ trusted
+    // yields a lot of verification burden about core::ptr::* that is a lot right now.
+    // We can come back to it, but I don't think flux even lets you write extern
+    // specs for those functions yet.
+    #[flux_rs::trusted]
     unsafe fn initialize_from_counts(
         base_ptr: NonNull<u8>,
         upcalls_num_val: UpcallItems,
@@ -350,6 +356,7 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> {
     /// which is guaranteed from align_of rust calls.
     #[flux_rs::opts(check_overflow = "none")] // TRUSTED: Not relevant for proof
     #[flux_rs::sig(fn(UpcallItems, AllowRoItems, AllowRwItems, GrantDataSize[@data_sz], GrantDataAlign{g: g > 0}) -> usize{alloc_sz: alloc_sz >= data_sz})]
+    #[flux_rs::no_panic]
     fn grant_size(
         upcalls_num: UpcallItems,
         allow_ro_num: AllowRoItems,
@@ -359,6 +366,7 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> {
     ) -> usize {
         #[flux_rs::trusted(reason = "arithmetic operation may overflow (bitwise arithmetic)")]
         #[flux_rs::sig(fn(usize, align:usize{0 < align}) -> usize{n: 0 < n && n < align})]
+        #[flux_rs::no_panic]
         fn calc_padding(kernel_managed_size: usize, align: usize) -> usize {
             // We know that grant_t_align is a power of 2, so we can make a mask
             // that will save only the remainder bits.
@@ -367,6 +375,8 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> {
             // Determine padding to get to the next multiple of grant_t_align by
             // taking the remainder and subtracting that from the alignment, then
             // ensuring a full alignment value maps to 0.
+            // Andrew note: This might overflow, but it seems that this is trusted and
+            // we don't care?
             (align - (kernel_managed_size & grant_t_align_mask)) & grant_t_align_mask
         }
 
@@ -384,6 +394,7 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> {
 
     /// Returns the alignment of the entire grant region based on the alignment
     /// of data T.
+    #[flux_rs::no_panic]
     fn grant_align(grant_t_align: GrantDataAlign) -> usize {
         // The kernel owned memory all aligned to usize. We need to use the
         // higher of the two alignment to ensure our padding calculations work
@@ -399,6 +410,8 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> {
     /// least the alignment of T and points to a grant that is of size
     /// grant_size bytes.
     #[flux_rs::sig(fn(NonNull<u8>, usize[@grant_sz], GrantDataSize{data_sz: data_sz <= grant_sz}) -> NonNull<u8>)]
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted]
     unsafe fn offset_of_grant_data_t(
         base_ptr: NonNull<u8>,
         grant_size: usize,
@@ -542,12 +555,14 @@ impl<'a, T: 'a + ?Sized> GrantData<'a, T> {
 
 impl<'a, T: 'a + ?Sized> Deref for GrantData<'a, T> {
     type Target = T;
+    #[flux_rs::no_panic]
     fn deref(&self) -> &T {
         self.data
     }
 }
 
 impl<'a, T: 'a + ?Sized> DerefMut for GrantData<'a, T> {
+    #[flux_rs::no_panic]
     fn deref_mut(&mut self) -> &mut T {
         self.data
     }
@@ -608,6 +623,7 @@ impl<'a> GrantKernelData<'a> {
     /// identified by the `subscribe_num`, which must match the subscribe number
     /// used when the upcall was originally subscribed by a process.
     /// `subscribe_num`s are indexed starting at zero.
+    #[flux_rs::no_panic]
     pub fn schedule_upcall(
         &self,
         subscribe_num: usize,
@@ -650,6 +666,7 @@ impl<'a> GrantKernelData<'a> {
     /// returns a [`crate::process::Error`] to allow for easy chaining of this
     /// function with the `ReadOnlyProcessBuffer::enter()` function with
     /// `and_then`.
+    #[flux_rs::no_panic]
     pub fn get_readonly_processbuffer(
         &self,
         allow_ro_num: usize,
@@ -691,6 +708,7 @@ impl<'a> GrantKernelData<'a> {
     /// returns a [`crate::process::Error`] to allow for easy chaining of this
     /// function with the `ReadWriteProcessBuffer::enter()` function with
     /// `and_then`.
+    #[flux_rs::no_panic]
     pub fn get_readwrite_processbuffer(
         &self,
         allow_rw_num: usize,
@@ -777,6 +795,8 @@ impl Default for SavedAllowRw {
 /// function is called. The memory does not need to be initialized yet. If it
 /// already does contain initialized memory, then those contents will be
 /// overwritten without being `Drop`ed first.
+#[flux_rs::no_panic]
+#[flux_rs::trusted]
 unsafe fn write_default_array<T: Default>(base: *mut T, num: usize) {
     for i in 0..num {
         base.add(i).write(T::default());
@@ -1012,6 +1032,8 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow
     /// If the grant is already allocated or could be allocated, and the process
     /// is valid, this returns `Ok(ProcessGrant)`. Otherwise it returns a
     /// relevant error.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted]
     fn new(
         grant: &Grant<T, Upcalls, AllowROs, AllowRWs>,
         processid: ProcessId,
@@ -1194,6 +1216,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow
     /// Return a [`ProcessGrant`] for a grant in a process if the process is
     /// valid and that process grant has already been allocated, or `None`
     /// otherwise.
+    #[flux_rs::no_panic]
     fn new_if_allocated(
         grant: &Grant<T, Upcalls, AllowROs, AllowRWs>,
         process: &'a dyn Process,
@@ -1218,6 +1241,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow
 
     /// Return the [`ProcessId`] of the process this [`ProcessGrant`] is
     /// associated with.
+    #[flux_rs::no_panic]
     pub fn processid(&self) -> ProcessId {
         self.process.processid()
     }
@@ -1232,6 +1256,11 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow
     /// Note, a grant can only be entered once at a time. Attempting to call
     /// `.enter()` on a grant while it is already entered will result in a
     /// `panic!()`. See the comment in `access_grant()` for more information.
+    // Andrew note: We need to actually add a no_panic spec which tracks if
+    // this grant is entered or not. The tricky part will be that entering
+    // a grant is implemented in the process, so I'm not sure how to handle this.
+    #[flux_rs::trusted]
+    #[flux_rs::no_panic]
     pub fn enter<F, R>(self, fun: F) -> R
     where
         F: FnOnce(&mut GrantData<T>, &GrantKernelData) -> R,
@@ -1732,6 +1761,7 @@ impl<T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: AllowRwSi
     /// This creates a [`ProcessGrant`] which is a handle for a grant allocated
     /// for a specific process. Then, that [`ProcessGrant`] is entered and the
     /// provided closure is run with access to the memory in the grant region.
+    #[flux_rs::no_panic]
     pub fn enter<F, R>(&self, processid: ProcessId, fun: F) -> Result<R, Error>
     where
         F: FnOnce(&mut GrantData<T>, &GrantKernelData) -> R,
@@ -1778,6 +1808,10 @@ impl<T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: AllowRwSi
     ///
     /// Calling this function when an [`ProcessGrant`] for a process is
     /// currently entered will result in a panic.
+    // Andrew note: placing `trusted` on this to work around FnMut::call_mut,
+    // and because we need to eventually come up with a no_panic spec for this.
+    #[flux_rs::trusted]
+    #[flux_rs::no_panic]
     pub fn each<F>(&self, mut fun: F)
     where
         F: FnMut(ProcessId, &mut GrantData<T>, &GrantKernelData),
@@ -1796,6 +1830,7 @@ impl<T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: AllowRwSi
     ///
     /// Calling this function when an [`ProcessGrant`] for a process is
     /// currently entered will result in a panic.
+    #[flux_rs::no_panic]
     #[flux_rs::trusted(reason = "ICE: assertion `left == right` failed `infer.rs:869`")]
     pub fn iter(&self) -> Iter<'_, T, Upcalls, AllowROs, AllowRWs> {
         Iter {
@@ -1828,6 +1863,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow
 {
     type Item = ProcessGrant<'a, T, Upcalls, AllowROs, AllowRWs>;
 
+    #[flux_rs::no_panic]
     fn next(&mut self) -> Option<Self::Item> {
         let grant = self.grant;
         // Get the next `ProcessId` from the kernel processes array that is
diff --git a/kernel/src/hil/gpio.rs b/kernel/src/hil/gpio.rs
index f974909e32..898ca4c512 100644
--- a/kernel/src/hil/gpio.rs
+++ b/kernel/src/hil/gpio.rs
@@ -96,6 +96,7 @@ pub trait Configure {
     /// Make the pin an input, returning the current configuration,
     /// which should be ither `Configuration::Input` or
     /// `Configuration::InputOutput`.
+    #[flux_rs::no_panic]
     fn make_input(&self) -> Configuration;
     /// Disable the pin as an input, returning the current configuration.
     fn disable_input(&self) -> Configuration;
@@ -109,6 +110,7 @@ pub trait Configure {
     fn deactivate_to_low_power(&self);
 
     /// Set the floating state of the pin.
+    #[flux_rs::no_panic]
     fn set_floating_state(&self, state: FloatingState);
     /// Return the current floating state of the pin.
     fn floating_state(&self) -> FloatingState;
@@ -180,9 +182,11 @@ pub trait Input {
     /// Get the current state of an input GPIO pin. For an output
     /// pin, return the output; for an input pin, return the input;
     /// for disabled or function pins the value is undefined.
+    #[flux_rs::no_panic]
     fn read(&self) -> bool;
 
     /// Get the current state of a GPIO pin, for a given activation mode.
+    #[flux_rs::no_panic]
     fn read_activation(&self, mode: ActivationMode) -> ActivationState {
         let value = self.read();
         match (mode, value) {
@@ -203,9 +207,11 @@ pub trait Interrupt<'a>: Input {
     /// Enable an interrupt on the GPIO pin. This does not
     /// configure the pin except to enable an interrupt: it
     /// should be separately configured as an input, etc.
+    #[flux_rs::no_panic]
     fn enable_interrupts(&self, mode: InterruptEdge);
 
     /// Disable interrupts for the GPIO pin.
+    #[flux_rs::no_panic]
     fn disable_interrupts(&self);
 
     /// Return whether this interrupt is pending
@@ -288,6 +294,7 @@ impl<'a, IP: InterruptPin<'a>> InterruptValueWrapper<'a, IP> {
 }
 
 impl<'a, IP: InterruptPin<'a>> InterruptWithValue<'a> for InterruptValueWrapper<'a, IP> {
+    #[flux_rs::no_panic]
     fn set_value(&self, value: u32) {
         self.value.set(value);
     }
@@ -304,11 +311,13 @@ impl<'a, IP: InterruptPin<'a>> InterruptWithValue<'a> for InterruptValueWrapper<
         self.source.is_pending()
     }
 
+    #[flux_rs::no_panic]
     fn enable_interrupts(&self, edge: InterruptEdge) -> Result<(), ErrorCode> {
         self.source.enable_interrupts(edge);
         Ok(())
     }
 
+    #[flux_rs::no_panic]
     fn disable_interrupts(&self) {
         self.source.disable_interrupts();
     }
@@ -333,6 +342,7 @@ impl<'a, IP: InterruptPin<'a>> Configure for InterruptValueWrapper<'a, IP> {
         self.source.disable_output()
     }
 
+    #[flux_rs::no_panic]
     fn make_input(&self) -> Configuration {
         self.source.make_input()
     }
@@ -345,6 +355,7 @@ impl<'a, IP: InterruptPin<'a>> Configure for InterruptValueWrapper<'a, IP> {
         self.source.deactivate_to_low_power();
     }
 
+    #[flux_rs::no_panic]
     fn set_floating_state(&self, state: FloatingState) {
         self.source.set_floating_state(state);
     }
diff --git a/kernel/src/hil/led.rs b/kernel/src/hil/led.rs
index 3589d0d315..5ca7be308d 100644
--- a/kernel/src/hil/led.rs
+++ b/kernel/src/hil/led.rs
@@ -16,15 +16,19 @@ use crate::hil::gpio;
 /// well.
 pub trait Led {
     /// Initialize the LED. Must be called before the LED is used.
+    #[flux_rs::no_panic]
     fn init(&self);
 
     /// Turn the LED on.
+    #[flux_rs::no_panic]
     fn on(&self);
 
     /// Turn the LED off.
+    #[flux_rs::no_panic]
     fn off(&self);
 
     /// Toggle the LED.
+    #[flux_rs::no_panic]
     fn toggle(&self);
 
     /// Return the on/off state of the LED. `true` if the LED is on, `false` if
diff --git a/kernel/src/hil/spi.rs b/kernel/src/hil/spi.rs
index 9731ebbc17..1cbea0a26a 100644
--- a/kernel/src/hil/spi.rs
+++ b/kernel/src/hil/spi.rs
@@ -435,6 +435,7 @@ pub trait SpiSlaveDevice<'a> {
     ///   - Err(INVAL): the `len` parameter is 0
     ///
     /// `Err` return values return the passed buffer `Option`s.
+    #[flux_rs::no_panic]
     fn read_write_bytes(
         &self,
         write_buffer: Option<&'static mut [u8]>,
@@ -453,8 +454,10 @@ pub trait SpiSlaveDevice<'a> {
     ///   - Err(BUSY): the SPI bus is busy with a `read_write_bytes`
     ///     operation whose callback hasn't been called yet.
     ///   - Err(FAIL): other failure
+    #[flux_rs::no_panic]
     fn set_polarity(&self, polarity: ClockPolarity) -> Result<(), ErrorCode>;
     /// Return the current bus polarity.
+    #[flux_rs::no_panic]
     fn get_polarity(&self) -> ClockPolarity;
 
     /// Set the bus phase (whether data is sent/received on leading or
@@ -463,8 +466,10 @@ pub trait SpiSlaveDevice<'a> {
     ///   - Err(BUSY): the SPI bus is busy with a `read_write_bytes`
     ///     operation whose callback hasn't been called yet.
     ///   - Err(FAIL): other failure
+    #[flux_rs::no_panic]
     fn set_phase(&self, phase: ClockPhase) -> Result<(), ErrorCode>;
 
     /// Return the current bus phase.
+    #[flux_rs::no_panic]
     fn get_phase(&self) -> ClockPhase;
 }
diff --git a/kernel/src/hil/time.rs b/kernel/src/hil/time.rs
index 7d3da0ac2c..8a625f593d 100644
--- a/kernel/src/hil/time.rs
+++ b/kernel/src/hil/time.rs
@@ -32,11 +32,13 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// The return value is a `u32`, in accordance with the bit widths
     /// specified using the BITS associated const on Rust integer
     /// types.
+    #[flux_rs::no_panic]
     fn width() -> u32;
 
     /// Converts the type into a `usize`, stripping the higher bits
     /// it if it is larger than `usize` and filling the higher bits
     /// with 0 if it is smaller than `usize`.
+    #[flux_rs::no_panic]
     fn into_usize(self) -> usize;
 
     /// The amount of bits required to left-justify this ticks value
@@ -44,6 +46,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// usize::BITS) - 1` bits. For timers with a `width` larger than
     /// usize, this value will be `0` (i.e., they can simply be
     /// truncated to usize::BITS bits).
+    #[flux_rs::no_panic]
     fn usize_padding() -> u32 {
         usize::BITS.saturating_sub(Self::width())
     }
@@ -64,6 +67,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// Convert the generic [`Frequency`] argument into a frequency
     /// (Hertz) describing a left-justified ticks value as returned by
     /// [`Ticks::into_usize_left_justified`].
+    #[flux_rs::no_panic]
     fn usize_left_justified_scale_freq<F: Frequency>() -> u32 {
         F::frequency() << Self::usize_padding()
     }
@@ -73,6 +77,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// with 0 if it is smaller than `u32`. Included as a simple
     /// helper since Tock uses `u32` pervasively and most platforms
     /// are 32 bits.
+    #[flux_rs::no_panic]
     fn into_u32(self) -> u32;
 
     /// The amount of bits required to left-justify this ticks value
@@ -84,6 +89,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// The return value is a `u32`, in accordance with the bit widths
     /// specified using the BITS associated const on Rust integer
     /// types.
+    #[flux_rs::no_panic]
     fn u32_padding() -> u32 {
         u32::BITS.saturating_sub(Self::width())
     }
@@ -97,6 +103,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// `2 ** u32_padding()`). Use `u32_left_justified_scale_freq` to
     /// convert the underlying timer's frequency into the padded ticks
     /// frequency in Hertz.
+    #[flux_rs::no_panic]
     fn into_u32_left_justified(self) -> u32 {
         self.into_u32() << Self::u32_padding()
     }
@@ -104,15 +111,18 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// Convert the generic [`Frequency`] argument into a frequency
     /// (Hertz) describing a left-justified ticks value as returned by
     /// [`Ticks::into_u32_left_justified`].
+    #[flux_rs::no_panic]
     fn u32_left_justified_scale_freq<F: Frequency>() -> u32 {
         F::frequency() << Self::u32_padding()
     }
 
     /// Add two values, wrapping around on overflow using standard
     /// unsigned arithmetic.
+    #[flux_rs::no_panic]
     fn wrapping_add(self, other: Self) -> Self;
     /// Subtract two values, wrapping around on underflow using standard
     /// unsigned arithmetic.
+    #[flux_rs::no_panic]
     fn wrapping_sub(self, other: Self) -> Self;
 
     /// Returns whether the value is in the range of [`start, `end`) using
@@ -120,6 +130,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
     /// if, incrementing from `start`, the value will be reached before `end`.
     /// Put another way, it returns `(self - start) < (end - start)` in
     /// unsigned arithmetic.
+    #[flux_rs::no_panic]
     fn within_range(self, start: Self, end: Self) -> bool;
 
     /// Returns the maximum value of this type, which should be (2^width)-1.
@@ -143,6 +154,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
 /// an associated type for an implementation of the `Time` trait.
 pub trait Frequency {
     /// Returns frequency in Hz.
+    #[flux_rs::no_panic]
     #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32;
 }
@@ -159,6 +171,7 @@ pub trait Time {
     /// a sample of a counter; if an implementation relies on
     /// it being constant or changing it should use `Timestamp`
     /// or `Counter`.
+    #[flux_rs::no_panic]
     fn now(&self) -> Self::Ticks;
 }
 
@@ -305,6 +318,7 @@ pub trait Alarm<'a>: Time {
     /// and `dt` rather than a single value denoting the counter value so it
     /// can distinguish between alarms which have very recently already
     /// passed and those in the far far future (see #1651).
+    #[flux_rs::no_panic]
     fn set_alarm(&self, reference: Self::Ticks, dt: Self::Ticks);
 
     /// Return the current alarm value. This is undefined at boot and
@@ -317,6 +331,7 @@ pub trait Alarm<'a>: Time {
     ///   the callback in the future
     ///   - `Err(ErrorCode::FAIL)` the alarm could not be disarmed and will invoke
     ///   the callback in the future
+    #[flux_rs::no_panic]
     fn disarm(&self) -> Result<(), ErrorCode>;
 
     /// Returns whether the alarm is currently armed. Note that this
diff --git a/kernel/src/hil/uart.rs b/kernel/src/hil/uart.rs
index 4614b1000d..439bd6ca12 100644
--- a/kernel/src/hil/uart.rs
+++ b/kernel/src/hil/uart.rs
@@ -115,6 +115,7 @@ pub trait Transmit<'a> {
     ///
     /// Calling `transmit_buffer` while there is an outstanding
     /// `transmit_buffer` or `transmit_word` operation will return BUSY.
+    #[flux_rs::no_panic]
     fn transmit_buffer(
         &self,
         tx_buffer: &'static mut [u8],
@@ -184,6 +185,7 @@ pub trait Receive<'a> {
     /// should use `receive_word`.  Calling `receive_buffer` while
     /// there is an outstanding `receive_buffer` or `receive_word`
     /// operation will return `Err(BUSY, rx_buffer)`.
+    #[flux_rs::no_panic]
     fn receive_buffer(
         &self,
         rx_buffer: &'static mut [u8],
@@ -215,6 +217,7 @@ pub trait Receive<'a> {
     /// of `CANCEL`.  If there was a reception outstanding, which is
     /// not cancelled successfully, then `FAIL` will be returned and
     /// there will be a later callback.
+    #[flux_rs::no_panic]
     fn receive_abort(&self) -> Result<(), ErrorCode>;
 }
 
diff --git a/kernel/src/kernel.rs b/kernel/src/kernel.rs
index 2caa39a857..9c2e4bb4a3 100644
--- a/kernel/src/kernel.rs
+++ b/kernel/src/kernel.rs
@@ -100,6 +100,7 @@ impl Kernel {
 
     /// Helper function that moves all non-generic portions of process_map_or
     /// into a non-generic function to reduce code bloat from monomorphization.
+    #[flux_rs::no_panic]
     pub(crate) fn get_process(&self, processid: ProcessId) -> Option<&dyn process::Process> {
         // We use the index in the [`ProcessId`] so we can do a direct lookup.
         // However, we are not guaranteed that the app still exists at that
@@ -129,6 +130,8 @@ impl Kernel {
     /// different index in the processes array. Note that a match _will_ be
     /// found if the process still exists in the correct location in the array
     /// but is in any "stopped" state.
+    #[flux_rs::trusted]
+    #[flux_rs::no_panic]
     pub(crate) fn process_map_or<F, R>(&self, default: R, processid: ProcessId, closure: F) -> R
     where
         F: FnOnce(&dyn process::Process) -> R,
diff --git a/kernel/src/process.rs b/kernel/src/process.rs
index e162fd74d9..a208ecba8f 100644
--- a/kernel/src/process.rs
+++ b/kernel/src/process.rs
@@ -94,6 +94,7 @@ pub struct ProcessId {
 }
 
 impl PartialEq for ProcessId {
+    #[flux_rs::no_panic]
     fn eq(&self, other: &ProcessId) -> bool {
         self.identifier == other.identifier
     }
@@ -330,6 +331,7 @@ impl BinaryVersion {
 /// schedule.
 pub trait Process {
     /// Returns the process's identifier.
+    #[flux_rs::no_panic]
     fn processid(&self) -> ProcessId;
 
     /// Returns the [`ShortId`] generated by the application binary checker at
@@ -371,6 +373,7 @@ pub trait Process {
     ///   there is insufficient space in the internal task queue.
     ///
     /// Other return values must be treated as kernel-internal errors.
+    #[flux_rs::no_panic]
     fn enqueue_task(&self, task: Task) -> Result<(), ErrorCode>;
 
     /// Remove the scheduled operation from the front of the queue and return it
@@ -694,6 +697,7 @@ pub trait Process {
     /// - There is not enough available memory to do the allocation, or
     /// - The grant_num is invalid, or
     /// - The grant_num already has an allocated grant.
+    #[flux_rs::no_panic]
     fn allocate_grant(
         &self,
         grant_num: usize,
@@ -706,6 +710,7 @@ pub trait Process {
     ///
     /// Returns `None` if the process is not active. Otherwise, returns `true`
     /// if the grant has been allocated, `false` otherwise.
+    #[flux_rs::no_panic]
     fn grant_is_allocated(&self, grant_num: usize) -> Option<bool>;
 
     /// Allocate memory from the grant region that is `size` bytes long and
@@ -731,6 +736,7 @@ pub trait Process {
     /// is invalid, if the grant has not been allocated, or if the grant is
     /// already entered. If this returns `Ok()` then the pointer points to the
     /// previously allocated memory for this grant.
+    #[flux_rs::no_panic]
     fn enter_grant(&self, grant_num: usize) -> Result<NonNull<u8>, Error>;
 
     /// Enter a custom grant based on the `identifier`.
diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs
index 63dc71083c..9dde6c3281 100644
--- a/kernel/src/processbuffer.rs
+++ b/kernel/src/processbuffer.rs
@@ -51,6 +51,8 @@ use flux_support::*;
 ///
 /// It is sound for multiple overlapping [`ReadableProcessSlice`]s or
 /// [`WriteableProcessSlice`]s to be in scope at the same time.
+#[flux_rs::trusted]
+#[flux_rs::no_panic]
 unsafe fn raw_processbuf_to_roprocessslice<'a>(
     ptr: FluxPtrU8Mut,
     len: usize,
@@ -158,6 +160,7 @@ pub trait ReadableProcessBuffer {
     /// # Default Process Buffer
     ///
     /// A default instance of a process buffer must return 0.
+    #[flux_rs::no_panic]
     fn len(&self) -> usize;
 
     /// Pointer to the first byte of the userspace memory region.
@@ -189,6 +192,7 @@ pub trait ReadableProcessBuffer {
     /// A default instance of a process buffer must return
     /// `Err(process::Error::NoSuchApp)` without executing the passed
     /// closure.
+    #[flux_rs::no_panic]
     fn enter<F, R>(&self, fun: F) -> Result<R, process::Error>
     where
         F: FnOnce(&ReadableProcessSlice) -> R;
@@ -311,6 +315,7 @@ impl ReadOnlyProcessBuffer {
 
 impl ReadableProcessBuffer for ReadOnlyProcessBuffer {
     /// Return the length of the buffer in bytes.
+    #[flux_rs::no_panic]
     fn len(&self) -> usize {
         self.process_id
             .map_or(0, |pid| pid.kernel.process_map_or(0, pid, |_| self.len))
@@ -329,6 +334,8 @@ impl ReadableProcessBuffer for ReadOnlyProcessBuffer {
     ///
     /// This verifies the process is still valid before accessing the underlying
     /// memory.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted]
     fn enter<F, R>(&self, fun: F) -> Result<R, process::Error>
     where
         F: FnOnce(&ReadableProcessSlice) -> R,
@@ -389,6 +396,8 @@ impl ReadOnlyProcessBufferRef<'_> {
     /// [`ReadOnlyProcessBuffer::new_external`]. The derived lifetime can
     /// help enforce the invariant that this incoming pointer may only
     /// be access for a certain duration.
+    #[flux_rs::trusted]
+    #[flux_rs::no_panic]
     pub(crate) unsafe fn new(ptr: FluxPtrU8Mut, len: usize, process_id: ProcessId) -> Self {
         Self {
             buf: ReadOnlyProcessBuffer::new(ptr, len, process_id),
@@ -399,6 +408,7 @@ impl ReadOnlyProcessBufferRef<'_> {
 
 impl Deref for ReadOnlyProcessBufferRef<'_> {
     type Target = ReadOnlyProcessBuffer;
+    #[flux_rs::no_panic]
     fn deref(&self) -> &Self::Target {
         &self.buf
     }
@@ -439,6 +449,7 @@ impl ReadWriteProcessBuffer {
     /// Refer to the safety requirements of
     /// [`ReadWriteProcessBuffer::new_external`].
     #[flux_rs::sig(fn (FluxPtrU8Mut[@ptr], len:usize{valid_size(ptr+len)}, ProcessId) -> Self)]
+    #[flux_rs::no_panic]
     pub(crate) unsafe fn new(ptr: FluxPtrU8Mut, len: usize, process_id: ProcessId) -> Self {
         ReadWriteProcessBuffer {
             ptr,
@@ -526,6 +537,7 @@ impl ReadWriteProcessBuffer {
 impl ReadableProcessBuffer for ReadWriteProcessBuffer {
     /// Return the length of the buffer in bytes.
     #[flux_rs::sig(fn (&Self[@p]) -> usize{len: valid_size(p.ptr + len)})]
+    #[flux_rs::no_panic]
     fn len(&self) -> usize {
         self.process_id
             .map_or(0, |pid| pid.kernel.process_map_or(0, pid, |_| self.len))
@@ -579,6 +591,8 @@ impl ReadableProcessBuffer for ReadWriteProcessBuffer {
 }
 
 impl WriteableProcessBuffer for ReadWriteProcessBuffer {
+    #[flux_rs::trusted]
+    #[flux_rs::no_panic]
     fn mut_enter<F, R>(&self, fun: F) -> Result<R, process::Error>
     where
         F: FnOnce(&WriteableProcessSlice) -> R,
@@ -636,6 +650,7 @@ impl ReadWriteProcessBufferRef<'_> {
     /// help enforce the invariant that this incoming pointer may only
     /// be access for a certain duration.
     #[flux_rs::sig(fn (FluxPtrU8Mut[@ptr], len:usize{valid_size(ptr+len)}, _) -> Self)]
+    #[flux_rs::no_panic]
     pub(crate) unsafe fn new(ptr: FluxPtrU8Mut, len: usize, process_id: ProcessId) -> Self {
         Self {
             buf: ReadWriteProcessBuffer::new(ptr, len, process_id),
@@ -646,6 +661,7 @@ impl ReadWriteProcessBufferRef<'_> {
 
 impl Deref for ReadWriteProcessBufferRef<'_> {
     type Target = ReadWriteProcessBuffer;
+    #[flux_rs::no_panic]
     fn deref(&self) -> &Self::Target {
         &self.buf
     }
@@ -683,6 +699,7 @@ pub struct ReadableProcessByte {
 
 impl ReadableProcessByte {
     #[inline]
+    #[flux_rs::no_panic]
     pub fn get(&self) -> u8 {
         self.cell.get()
     }
@@ -705,6 +722,8 @@ pub struct ReadableProcessSlice {
     slice: [ReadableProcessByte],
 }
 
+#[flux_rs::trusted]
+#[flux_rs::no_panic]
 fn cast_byte_slice_to_process_slice(byte_slice: &[ReadableProcessByte]) -> &ReadableProcessSlice {
     // As ReadableProcessSlice is a transparent wrapper around its inner type,
     // [ReadableProcessByte], we can safely transmute a reference to the inner
@@ -798,11 +817,13 @@ impl ReadableProcessSlice {
     }
 
     /// Return the length of the slice in bytes.
+    #[flux_rs::no_panic]
     pub fn len(&self) -> usize {
         self.slice.len()
     }
 
     /// Return an iterator over the bytes of the slice.
+    #[flux_rs::no_panic]
     pub fn iter(&self) -> core::slice::Iter<'_, ReadableProcessByte> {
         self.slice.iter()
     }
@@ -820,6 +841,7 @@ impl ReadableProcessSlice {
 
     /// Access a portion of the slice with bounds checking. If the access is not
     /// within the slice then `None` is returned.
+    #[flux_rs::no_panic]
     pub fn get(&self, range: Range<usize>) -> Option<&ReadableProcessSlice> {
         if let Some(slice) = self.slice.get(range) {
             Some(cast_byte_slice_to_process_slice(slice))
@@ -853,6 +875,7 @@ impl Index<Range<usize>> for ReadableProcessSlice {
     // Subslicing will still yield a ReadableProcessSlice reference
     type Output = Self;
 
+    #[flux_rs::no_panic]
     fn index(&self, idx: Range<usize>) -> &Self::Output {
         cast_byte_slice_to_process_slice(&self.slice[idx])
     }
@@ -907,6 +930,8 @@ pub struct WriteableProcessSlice {
     slice: [Cell<u8>],
 }
 
+#[flux_rs::trusted]
+#[flux_rs::no_panic]
 fn cast_cell_slice_to_process_slice(cell_slice: &[Cell<u8>]) -> &WriteableProcessSlice {
     // # Safety
     //
@@ -1039,11 +1064,13 @@ impl WriteableProcessSlice {
     }
 
     /// Return the length of the slice in bytes.
+    #[flux_rs::no_panic]
     pub fn len(&self) -> usize {
         self.slice.len()
     }
 
     /// Return an iterator over the slice.
+    #[flux_rs::no_panic]
     pub fn iter(&self) -> core::slice::Iter<'_, Cell<u8>> {
         self.slice.iter()
     }
@@ -1094,6 +1121,7 @@ impl Index<Range<usize>> for WriteableProcessSlice {
     // Subslicing will still yield a WriteableProcessSlice reference.
     type Output = Self;
 
+    #[flux_rs::no_panic]
     fn index(&self, idx: Range<usize>) -> &Self::Output {
         cast_cell_slice_to_process_slice(&self.slice[idx])
     }
@@ -1124,6 +1152,7 @@ impl Index<usize> for WriteableProcessSlice {
 
     #[flux_rs::trusted_impl(reason = "needs associated refinement on Index trait")]
     #[flux_rs::sig(fn(self: &WriteableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)]
+    #[flux_rs::no_panic]
     fn index(&self, idx: usize) -> &Self::Output {
         // As WriteableProcessSlice is a transparent wrapper around
         // its inner type, [Cell<u8>], we can use the regular slicing
diff --git a/kernel/src/syscall_driver.rs b/kernel/src/syscall_driver.rs
index e37f3f239b..abfa4d8370 100644
--- a/kernel/src/syscall_driver.rs
+++ b/kernel/src/syscall_driver.rs
@@ -30,6 +30,7 @@ impl CommandReturn {
     }
 
     /// Command error
+    #[flux_rs::no_panic]
     pub fn failure(rc: ErrorCode) -> Self {
         CommandReturn(SyscallReturn::Failure(rc))
     }
@@ -50,11 +51,13 @@ impl CommandReturn {
     }
 
     /// Successful command
+    #[flux_rs::no_panic]
     pub fn success() -> Self {
         CommandReturn(SyscallReturn::Success)
     }
 
     /// Successful command with an additional 32-bit data field
+    #[flux_rs::no_panic]
     pub fn success_u32(data0: u32) -> Self {
         CommandReturn(SyscallReturn::SuccessU32(data0))
     }
diff --git a/kernel/src/upcall.rs b/kernel/src/upcall.rs
index a719f3d37d..ffcf6b1da9 100644
--- a/kernel/src/upcall.rs
+++ b/kernel/src/upcall.rs
@@ -95,6 +95,7 @@ pub(crate) struct Upcall {
 }
 
 impl Upcall {
+    #[flux_rs::no_panic]
     pub(crate) fn new(
         process_id: ProcessId,
         upcall_id: UpcallId,
@@ -124,6 +125,13 @@ impl Upcall {
     /// parameter so we take advantage of it. If in the future that is not the
     /// case we could have `process` be an Option and just do the search with
     /// the stored [`ProcessId`].
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted]
+    // Andrew note: marking this as trusted because the debug! call introduces
+    // verification burden to annotated core::fmt::rt::blah as no_panic!.
+    // The symbols referred to in core::fmt::rt are things like new_v1_formatted,
+    // which may have been patched out? In any case, it's hard to get working on
+    // my machine.
     pub(crate) fn schedule(
         &self,
         process: &dyn process::Process,
diff --git a/libraries/tock-cells/Cargo.toml b/libraries/tock-cells/Cargo.toml
index 882e8540f0..1937d6d03f 100644
--- a/libraries/tock-cells/Cargo.toml
+++ b/libraries/tock-cells/Cargo.toml
@@ -11,3 +11,11 @@ edition = "2021"
 
 [lints]
 workspace = true
+
+[dependencies]
+flux-rs = { git  = "https://github.com/flux-rs/flux.git" }
+flux_support = { path = "../../flux_support" }
+
+[package.metadata.flux]
+enabled = true
+check_overflow = "lazy"
\ No newline at end of file
diff --git a/libraries/tock-cells/src/optional_cell.rs b/libraries/tock-cells/src/optional_cell.rs
index b0e15e5c11..29b7b95a48 100644
--- a/libraries/tock-cells/src/optional_cell.rs
+++ b/libraries/tock-cells/src/optional_cell.rs
@@ -6,6 +6,8 @@
 
 use core::cell::Cell;
 
+use flux_support::*;
+
 /// `OptionalCell` is a `Cell` that wraps an `Option`. This is helper type
 /// that makes keeping types that can be `None` a little cleaner.
 pub struct OptionalCell<T> {
@@ -14,6 +16,7 @@ pub struct OptionalCell<T> {
 
 impl<T> OptionalCell<T> {
     /// Create a new OptionalCell.
+    #[flux_rs::no_panic]
     pub const fn new(val: T) -> OptionalCell<T> {
         OptionalCell {
             value: Cell::new(Some(val)),
@@ -21,6 +24,7 @@ impl<T> OptionalCell<T> {
     }
 
     /// Create an empty `OptionalCell` (contains just `None`).
+    #[flux_rs::no_panic]
     pub const fn empty() -> OptionalCell<T> {
         OptionalCell {
             value: Cell::new(None),
@@ -28,6 +32,7 @@ impl<T> OptionalCell<T> {
     }
 
     /// Update the stored value.
+    #[flux_rs::no_panic]
     pub fn set(&self, val: T) {
         self.value.set(Some(val));
     }
@@ -48,11 +53,13 @@ impl<T> OptionalCell<T> {
     }
 
     /// Reset the stored value to `None`.
+    #[flux_rs::no_panic]
     pub fn clear(&self) {
         self.value.set(None);
     }
 
     /// Check if the cell contains something.
+    #[flux_rs::no_panic]
     pub fn is_some(&self) -> bool {
         let value = self.value.take();
         let out = value.is_some();
@@ -61,6 +68,7 @@ impl<T> OptionalCell<T> {
     }
 
     /// Check if the cell is None.
+    #[flux_rs::no_panic]
     pub fn is_none(&self) -> bool {
         let value = self.value.take();
         let out = value.is_none();
@@ -137,6 +145,7 @@ impl<T> OptionalCell<T> {
     }
 
     /// Return the contained value and replace it with None.
+    #[flux_rs::no_panic]
     pub fn take(&self) -> Option<T> {
         self.value.take()
     }
@@ -211,6 +220,8 @@ impl<T: Copy> OptionalCell<T> {
     }
 
     /// Call a closure on the value if the value exists.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted]
     pub fn map<F, R>(&self, closure: F) -> Option<R>
     where
         F: FnOnce(T) -> R,
@@ -220,6 +231,8 @@ impl<T: Copy> OptionalCell<T> {
 
     /// Call a closure on the value if the value exists, or return the
     /// default if the value is `None`.
+    #[flux_rs::no_panic]
+    #[flux_rs::trusted]
     pub fn map_or<F, R>(&self, default: R, closure: F) -> R
     where
         F: FnOnce(T) -> R,
diff --git a/libraries/tock-cells/src/take_cell.rs b/libraries/tock-cells/src/take_cell.rs
index d52e01d5ae..f220c1eba5 100644
--- a/libraries/tock-cells/src/take_cell.rs
+++ b/libraries/tock-cells/src/take_cell.rs
@@ -24,17 +24,20 @@ impl<'a, T: ?Sized> TakeCell<'a, T> {
         val: Cell::new(None),
     };
 
+    #[flux_rs::no_panic]
     pub const fn empty() -> TakeCell<'a, T> {
         Self::EMPTY
     }
 
     /// Creates a new `TakeCell` containing `value`
+    #[flux_rs::no_panic]
     pub fn new(value: &'a mut T) -> TakeCell<'a, T> {
         TakeCell {
             val: Cell::new(Some(value)),
         }
     }
 
+    #[flux_rs::no_panic]
     pub fn is_none(&self) -> bool {
         let inner = self.take();
         let return_val = inner.is_none();
@@ -64,17 +67,20 @@ impl<'a, T: ?Sized> TakeCell<'a, T> {
     /// x.take();
     /// assert_eq!(y.take(), None);
     /// ```
+    #[flux_rs::no_panic]
     pub fn take(&self) -> Option<&'a mut T> {
         self.val.replace(None)
     }
 
     /// Stores `val` in the `TakeCell`
+    #[flux_rs::no_panic]
     pub fn put(&self, val: Option<&'a mut T>) {
         self.val.replace(val);
     }
 
     /// Replaces the contents of the `TakeCell` with `val`. If the cell was not
     /// empty, the previous value is returned, otherwise `None` is returned.
+    #[flux_rs::no_panic]
     pub fn replace(&self, val: &'a mut T) -> Option<&'a mut T> {
         self.val.replace(Some(val))
     }
@@ -125,6 +131,8 @@ impl<'a, T: ?Sized> TakeCell<'a, T> {
     }
 
     /// Performs a `map` or returns a default value if the `TakeCell` is empty
+    #[flux_rs::trusted] // Andrew: marking as trusted because of FnOnce::call_once
+    #[flux_rs::no_panic]
     pub fn map_or<F, R>(&self, default: R, closure: F) -> R
     where
         F: FnOnce(&mut T) -> R,