diff --git a/hal/src/mailbox.rs b/hal/src/mailbox.rs
index 53c996a..c3bcefb 100644
--- a/hal/src/mailbox.rs
+++ b/hal/src/mailbox.rs
@@ -1,45 +1,66 @@
 //! Matcha hardware mailbox.
-//! TODO(aappleby): Rework this to match the RTL implementation.
 
 use core::mem::transmute;
-use kernel::common::registers::{register_structs, ReadWrite};
+use kernel::common::registers::{register_structs, ReadOnly, ReadWrite, WriteOnly};
 use kernel::common::StaticRef;
 
-use crate::dprintf;
 use crate::*;
 
+// TODO(aappleby): These constants are hardcoded pending the merge of the
+// mailbox RTL.
+
 pub const MAILBOX0_BASE: u32 = 0x400F0000;
 pub const MAILBOX1_BASE: u32 = 0x400F1000;
-pub const MAILBOX_SIZE_DWORDS: usize = 8;
+pub const MAILBOX_SIZE_DWORDS: u32 = 8;
+pub const MAILBOX_STATUS_HIWATER: u32 = 0b0100;
+pub const MAILBOX_STATUS_LOWATER: u32 = 0b1000;
+
+pub const MAILBOX0_HIWATER_IRQ: isize = 100;
+pub const MAILBOX0_LOWATER_IRQ: isize = 101;
+
+pub const MAILBOX1_HIWATER_IRQ: isize = 102;
+pub const MAILBOX1_LOWATER_IRQ: isize = 103;
+
+pub const IRQ_ERROR : u32 = 0b001;
+pub const IRQ_HIWATER : u32 = 0b010;
+pub const IRQ_LOWATER : u32 = 0b100;
 
 register_structs! {
   pub MailboxRegisters {
-      (0x000 => message: [ReadWrite<u32>; 8]),
-      (0x020 => irq_send: ReadWrite<u32>),
-      (0x024 => irq_recv: ReadWrite<u32>),
+      (0x000 => reg_istate:  ReadWrite<u32>),
+      (0x004 => reg_ienable: ReadWrite<u32>),
+      (0x008 => reg_itest:   ReadWrite<u32>),
+      (0x00C => reg_write:   WriteOnly<u32>),
+      (0x010 => reg_read:    ReadOnly<u32>),
+      (0x014 => reg_status:  ReadOnly<u32>),
+      (0x018 => reg_error:   ReadOnly<u32>),
+      (0x01C => reg_hiwater: ReadWrite<u32>),
+      (0x020 => reg_lowater: ReadWrite<u32>),
+      (0x024 => reg_flush:   WriteOnly<u32>),
       (0x028 => @END),
   }
 }
 
 pub struct Mailbox {
     regs: StaticRef<MailboxRegisters>,
-    plic_irq_send: isize,
-    plic_irq_recv: isize,
+    plic_irq_hiwater: isize,
+    plic_irq_lowater: isize,
 }
 
 pub const MAILBOX0: Mailbox = Mailbox {
     regs: unsafe { StaticRef::new(MAILBOX0_BASE as *mut MailboxRegisters) },
-    plic_irq_send: 100,
-    plic_irq_recv: 101,
+    plic_irq_hiwater: MAILBOX0_HIWATER_IRQ,
+    plic_irq_lowater: MAILBOX0_LOWATER_IRQ,
 };
 
 pub const MAILBOX1: Mailbox = Mailbox {
     regs: unsafe { StaticRef::new(MAILBOX1_BASE as *mut MailboxRegisters) },
-    plic_irq_send: 102,
-    plic_irq_recv: 103,
+    plic_irq_hiwater: MAILBOX1_HIWATER_IRQ,
+    plic_irq_lowater: MAILBOX1_LOWATER_IRQ,
 };
 
-// 32-bit-word bitfield helper for the PLIC's irq enable lines.
+// 32-bit-word bitfield helpers for the PLIC's irq enable lines.
+
 pub unsafe fn set_bit(base: u32, bit_index: isize) {
     let buf: *mut u32 = transmute(base);
     let mut bits = buf.offset(bit_index >> 5).read_volatile();
@@ -47,30 +68,50 @@
     buf.offset(bit_index >> 5).write_volatile(bits);
 }
 
-impl Mailbox {
-    pub unsafe fn get_message(&self, message: &mut [u32]) {
-        if message.len() > MAILBOX_SIZE_DWORDS {
-            dprintf!("get_message() - Bad message size {}\n", message.len());
-            return;
-        }
+pub unsafe fn clear_bit(base: u32, bit_index: isize) {
+    let buf: *mut u32 = transmute(base);
+    let mut bits = buf.offset(bit_index >> 5).read_volatile();
+    bits &= !(1 << (bit_index & 31));
+    buf.offset(bit_index >> 5).write_volatile(bits);
+}
 
-        // Empty the mailbox - must be done with dword-sized writes
+impl Mailbox {
+    pub unsafe fn send_message(&self, message: &[u32]) {
+        self.regs.reg_lowater.set(MAILBOX_SIZE_DWORDS - 1);
+        self.regs.reg_ienable.set(IRQ_LOWATER);
         for i in 0..message.len() {
-            message[i] = self.regs.message[i].get();
-            self.regs.message[i].set(0);
+            self.wait_irq_lowater();
+            self.regs.reg_write.set(message[i]);
         }
+        self.regs.reg_ienable.set(0);
+        self.regs.reg_lowater.set(0);
     }
 
-    pub unsafe fn set_message(&self, message: &[u32]) {
-        if message.len() > MAILBOX_SIZE_DWORDS {
-            dprintf!("set_message() - Bad message size {}\n", message.len());
-            return;
-        }
-
-        // Fill the mailbox - must be done with dword-sized writes
+    pub unsafe fn recv_message(&self, message: &mut [u32]) {
+        self.regs.reg_hiwater.set(1);
+        self.regs.reg_ienable.set(IRQ_HIWATER);
         for i in 0..message.len() {
-            self.regs.message[i].set(message[i]);
+            self.wait_irq_hiwater();
+            message[i] = self.regs.reg_read.get();
         }
+        self.regs.reg_ienable.set(0);
+        self.regs.reg_hiwater.set(0);
+    }
+
+    pub unsafe fn wait_hiwater(&self, hiwater : u32) {
+        self.regs.reg_hiwater.set(hiwater);
+        self.regs.reg_ienable.set(IRQ_HIWATER);
+        self.wait_irq_hiwater();
+        self.regs.reg_ienable.set(0);
+        self.regs.reg_hiwater.set(0);
+    }
+
+    pub unsafe fn wait_lowater(&self, lowater : u32) {
+        self.regs.reg_lowater.set(lowater);
+        self.regs.reg_ienable.set(IRQ_LOWATER);
+        self.wait_irq_lowater();
+        self.regs.reg_ienable.set(0);
+        self.regs.reg_lowater.set(0);
     }
 
     // This requires a small bit of explanation - if an interrupt were to happen
@@ -80,64 +121,29 @@
     // an interrupt has been triggered, 'wfi' will continue and the isr will
     // execute immediately after global interrupts are re-enabled.
 
-    unsafe fn wait_until_full(&self) {
-        while self.regs.irq_send.get() == 0 {
+    unsafe fn wait_irq_hiwater(&self) {
+        while (self.regs.reg_status.get() & MAILBOX_STATUS_HIWATER) == 0 {
             clear_mstatus_bits(MIE_BIT | SIE_BIT);
-            if self.regs.irq_send.get() == 0 {
+            set_bit(plic::PLIC_EN0, self.plic_irq_hiwater);
+            if (self.regs.reg_status.get() & MAILBOX_STATUS_HIWATER) == 0 {
                 asm!("wfi");
             }
+            clear_bit(plic::PLIC_EN0, self.plic_irq_hiwater);
             set_mstatus_bits(MIE_BIT | SIE_BIT);
         }
+        self.regs.reg_istate.set(IRQ_HIWATER);
     }
 
-    unsafe fn wait_until_empty(&self) {
-        while self.regs.irq_send.get() != 0 {
+    unsafe fn wait_irq_lowater(&self) {
+        while (self.regs.reg_status.get() & MAILBOX_STATUS_LOWATER) == 0 {
             clear_mstatus_bits(MIE_BIT | SIE_BIT);
-            if self.regs.irq_send.get() != 0 {
+            set_bit(plic::PLIC_EN0, self.plic_irq_lowater);
+            if (self.regs.reg_status.get() & MAILBOX_STATUS_LOWATER) == 0 {
                 asm!("wfi");
             }
+            clear_bit(plic::PLIC_EN0, self.plic_irq_lowater);
             set_mstatus_bits(MIE_BIT | SIE_BIT);
         }
-    }
-
-    unsafe fn wait_until_recv(&self) {
-        while self.regs.irq_recv.get() == 0 {
-            clear_mstatus_bits(MIE_BIT | SIE_BIT);
-            if self.regs.irq_recv.get() == 0 {
-                asm!("wfi");
-            }
-            set_mstatus_bits(MIE_BIT | SIE_BIT);
-        }
-    }
-
-    pub unsafe fn send_message(&self, message: &[u32], wait_for_ack: bool) {
-        self.wait_until_empty();
-        self.set_message(message);
-        self.regs.irq_send.set(1);
-
-        if wait_for_ack {
-            // Enable the RECV irq line, then wait for RECV. The ISR will disable the
-            // irq line once it fires.
-            set_bit(plic::PLIC_EN0, self.plic_irq_recv);
-            self.wait_until_recv();
-            self.regs.irq_recv.set(0);
-        }
-    }
-
-    // TODO(aappleby): Refactor
-    pub unsafe fn recv_message(&self, message: &mut [u32], send_ack: bool) {
-        // Enable the SEND irq line and wait for new mail. The ISR will disable the
-        // irq line once it fires.
-        // set_bit(plic::PLIC_EN1, self.plic_irq_send);
-        self.wait_until_full();
-        self.regs.irq_send.set(0);
-
-        // Message has arrived.
-        self.get_message(message);
-
-        if send_ack {
-            // Trigger RECV
-            self.regs.irq_recv.set(1);
-        }
+        self.regs.reg_istate.set(IRQ_LOWATER);
     }
 }
diff --git a/utils/src/lib.rs b/utils/src/lib.rs
index a8cd612..546bbb9 100644
--- a/utils/src/lib.rs
+++ b/utils/src/lib.rs
@@ -19,45 +19,58 @@
         let sel4_elf = elf_loader::find_elf("kernel");
         let capdl_elf = elf_loader::find_elf("capdl-loader");
 
-        // If we found all of them, boot in Shodan mode.
-        if !sel4_elf.is_null() && !capdl_elf.is_null() {
-            dprintf!("Loading seL4 kernel elf\n");
-            elf_loader::load_elf_segments(sel4_elf.as_ref().unwrap(), 0);
-
-            let sel4_segments = elf_loader::elf_get_segments(sel4_elf);
-            let capdl_segments = elf_loader::elf_get_segments(capdl_elf);
-
-            let sel4_pend = round_up_to_page(elf_loader::elf_phys_max(sel4_segments));
-
-            dprintf!("Loading capdl-loader to the page after seL4\n");
-            elf_loader::load_elf_segments(
-                capdl_elf.as_ref().unwrap(),
-                sel4_pend - elf_loader::elf_phys_min(capdl_segments),
-            );
-
-            dprintf!("Starting management core\n");
-
-            let entry_point: u32 = (*sel4_elf).e_entry
-                - (elf_loader::elf_virt_min(sel4_segments)
-                    - elf_loader::elf_phys_min(sel4_segments));
-
-            let message = [
-                transmute(sel4_pend),
-                transmute(
-                    sel4_pend
-                        + round_up_to_page(
-                            elf_loader::elf_phys_max(capdl_segments)
-                                - elf_loader::elf_phys_min(capdl_segments),
-                        ),
-                ),
-                transmute(sel4_pend - elf_loader::elf_phys_min(capdl_segments)),
-                transmute((*capdl_elf).e_entry),
-            ];
-            matcha_hal::mailbox::MAILBOX1.set_message(&message);
-
-            SMC_CONTROL_BLOCK.write_volatile(entry_point);
-        } else {
-            dprintf!("Missing sel4_elf or capdl_elf\n");
+        if sel4_elf.is_null() {
+          dprintf!("Boot failure, seL4 kernel ELF missing.\n");
+          return;
         }
+
+        if capdl_elf.is_null() {
+          dprintf!("Boot failure seL4 CapDL ELF missing.\n");
+          return;
+        }
+
+        // If we found all of them, boot in Shodan mode.
+        dprintf!("Loading seL4 kernel elf\n");
+        elf_loader::load_elf_segments(sel4_elf.as_ref().unwrap(), 0);
+
+        let sel4_segments = elf_loader::elf_get_segments(sel4_elf);
+        let capdl_segments = elf_loader::elf_get_segments(capdl_elf);
+
+        let sel4_pend = round_up_to_page(elf_loader::elf_phys_max(sel4_segments));
+
+        dprintf!("Loading capdl-loader to the page after seL4\n");
+        elf_loader::load_elf_segments(
+            capdl_elf.as_ref().unwrap(),
+            sel4_pend - elf_loader::elf_phys_min(capdl_segments),
+        );
+
+        dprintf!("Starting management core\n");
+
+        let entry_point: u32 = (*sel4_elf).e_entry
+            - (elf_loader::elf_virt_min(sel4_segments)
+                - elf_loader::elf_phys_min(sel4_segments));
+
+        let message = [
+            transmute(sel4_pend),
+            transmute(
+                sel4_pend
+                    + round_up_to_page(
+                        elf_loader::elf_phys_max(capdl_segments)
+                            - elf_loader::elf_phys_min(capdl_segments),
+                    ),
+            ),
+            transmute(sel4_pend - elf_loader::elf_phys_min(capdl_segments)),
+            transmute((*capdl_elf).e_entry),
+        ];
+        matcha_hal::mailbox::MAILBOX1.send_message(&message);
+        dprintf!("seL4 boot message posted\n");
+
+        SMC_CONTROL_BLOCK.write_volatile(entry_point);
+
+        dprintf!("SMC started, waiting on mailbox to clear\n");
+
+        matcha_hal::mailbox::MAILBOX1.wait_lowater(0);
+
+        dprintf!("Mailbox cleared\n");
     }
 }