diff --git a/kernel/src/deferred_call.rs b/kernel/src/deferred_call.rs
index de1367c0b1..6beb6bd8c2 100644
--- a/kernel/src/deferred_call.rs
+++ b/kernel/src/deferred_call.rs
@@ -79,6 +79,7 @@ pub trait DeferredCallClient: Sized {
 /// (e.g. `&dyn DeferredCall`). Using a trait object, will include a 20 byte vtable
 /// per instance, but this alternative stores only the data and function pointers,
 /// 8 bytes per instance.
+#[flux::opaque]
 #[derive(Copy, Clone)]
 struct DynDefCallRef<'a> {
     data: *const (),
diff --git a/kernel/src/ipc.rs b/kernel/src/ipc.rs
index 06c0c8b7f7..fdc6d89af9 100644
--- a/kernel/src/ipc.rs
+++ b/kernel/src/ipc.rs
@@ -46,7 +46,6 @@ pub struct IPC<const NUM_PROCS: u8> {
     /// The grant regions for each process that holds the per-process IPC data.
     data: Grant<IPCData, UpcallCount<NUM_PROCS>, AllowRoCount<1>, AllowRwCount<NUM_PROCS>>,
 }
-
 impl<const NUM_PROCS: u8> IPC<NUM_PROCS> {
     pub fn new(
         kernel: &'static Kernel,
@@ -60,6 +59,7 @@ impl<const NUM_PROCS: u8> IPC<NUM_PROCS> {
 
     /// Schedule an IPC upcall for a process. This is called by the main
     /// scheduler loop if an IPC task was queued for the process.
+    #[flux::trusted]
     pub(crate) unsafe fn schedule_upcall(
         &self,
         schedule_on: ProcessId,
@@ -119,6 +119,7 @@ impl<const NUM_PROCS: u8> SyscallDriver for IPC<NUM_PROCS> {
     /// - `3`: Notify a client with descriptor `target_id`, typically in response to a previous
     ///        notify from the client. Returns an error if `target_id` refers to an invalid client
     ///        or the notify fails to enqueue.
+    #[flux::trusted]
     fn command(
         &self,
         command_number: usize,
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index 05227bdec9..ed8e2f4bb3 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -108,16 +108,15 @@ pub mod capabilities;
 pub mod collections;
 pub mod component;
 pub mod debug;
-#[flux::ignore]
+#[flux::ignore] // Uses pointers in a way that flux doesn't like
 pub mod deferred_call;
 pub mod errorcode;
 #[flux::trusted]
 pub mod grant;
-#[flux::ignore]
+#[flux::ignore] // Waiting on dyn trait objects
 pub mod hil;
 #[flux::ignore]
 pub mod introspection;
-#[flux::trusted]
 pub mod ipc;
 pub mod platform;
 pub mod process;
@@ -138,7 +137,6 @@ mod process_binary;
 #[flux::ignore]
 mod process_loading;
 mod process_policies;
-#[flux::ignore]
 mod process_printer;
 #[flux::ignore]
 mod process_standard;
diff --git a/kernel/src/process_printer.rs b/kernel/src/process_printer.rs
index a5e68af7af..8126044a5b 100644
--- a/kernel/src/process_printer.rs
+++ b/kernel/src/process_printer.rs
@@ -55,6 +55,7 @@ pub trait ProcessPrinter {
     /// ready to accept more data. If `print_overview()` returns `None`, the
     /// `writer` indicated it accepted all output and the caller does not need
     /// to call `print_overview()` again to finish the printing.
+    #[flux::ignore]
     fn print_overview(
         &self,
         process: &TockProc<'_>,
@@ -98,6 +99,7 @@ impl ProcessPrinter for ProcessPrinterText {
     //    being duplicated. However, it does not make sense that the kernel
     //    would want to run the process while it is displaying debugging
     //    information about it, so this should be a safe assumption.
+    #[flux::ignore]
     fn print_overview(
         &self,
         process: &TockProc<'_>,