diff --git a/hal/src/mailbox.rs b/hal/src/mailbox.rs
index c3bcefb..d4acf4b 100644
--- a/hal/src/mailbox.rs
+++ b/hal/src/mailbox.rs
@@ -1,62 +1,63 @@
 //! Matcha hardware mailbox.
 
+// We want constants & registers to stay together even if they're not currently
+// used in this file.
+#![allow(dead_code)]
+
 use core::mem::transmute;
 use kernel::common::registers::{register_structs, ReadOnly, ReadWrite, WriteOnly};
 use kernel::common::StaticRef;
 
 use crate::*;
 
-// TODO(aappleby): These constants are hardcoded pending the merge of the
-// mailbox RTL.
+const MAILBOX_BASE: u32 = 0x40800000; // TOP_MATCHA_MAILBOX_SEC_BASE_ADDR
+const MAILBOX_WTIRQ: u32 = 181; // kTopMatchaPlicIrqIdMailboxSecWtirq
+const MAILBOX_RTIRQ: u32 = 182; // kTopMatchaPlicIrqIdMailboxSecRtirq
+const MAILBOX_EIRQ: u32 = 183; // kTopMatchaPlicIrqIdMailboxSecEirq
 
-pub const MAILBOX0_BASE: u32 = 0x400F0000;
-pub const MAILBOX1_BASE: u32 = 0x400F1000;
-pub const MAILBOX_SIZE_DWORDS: u32 = 8;
-pub const MAILBOX_STATUS_HIWATER: u32 = 0b0100;
-pub const MAILBOX_STATUS_LOWATER: u32 = 0b1000;
+const MAILBOX_SIZE_DWORDS: u32 = 8;
 
-pub const MAILBOX0_HIWATER_IRQ: isize = 100;
-pub const MAILBOX0_LOWATER_IRQ: isize = 101;
+const INTR_STATE_BIT_WTIRQ: u32 = 0b001;
+const INTR_STATE_BIT_RTIRQ: u32 = 0b010;
+const INTR_STATE_BIT_EIRQ: u32 = 0b100;
 
-pub const MAILBOX1_HIWATER_IRQ: isize = 102;
-pub const MAILBOX1_LOWATER_IRQ: isize = 103;
+const INTR_ENABLE_BIT_WTIRQ: u32 = 0b001;
+const INTR_ENABLE_BIT_RTIRQ: u32 = 0b010;
+const INTR_ENABLE_BIT_EIRQ: u32 = 0b100;
 
-pub const IRQ_ERROR : u32 = 0b001;
-pub const IRQ_HIWATER : u32 = 0b010;
-pub const IRQ_LOWATER : u32 = 0b100;
+const STATUS_BIT_EMPTY: u32 = 0b0001;
+const STATUS_BIT_FULL: u32 = 0b0010;
+const STATUS_BIT_WFIFOL: u32 = 0b0100;
+const STATUS_BIT_RFIFOL: u32 = 0b1000;
 
 register_structs! {
-  pub MailboxRegisters {
-      (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 MailboxRegisters {
+        (0x000 => reg_intr_state:  ReadWrite<u32>),
+        (0x004 => reg_intr_enable: ReadWrite<u32>),
+        (0x008 => reg_intr_test:   ReadWrite<u32>),
+        (0x00C => reg_mboxw:       WriteOnly<u32>),
+        (0x010 => reg_mboxr:       ReadOnly<u32>),
+        (0x014 => reg_status:      ReadOnly<u32>),
+        (0x018 => reg_error:       ReadOnly<u32>),
+        (0x01C => reg_wirqt:       ReadWrite<u32>),
+        (0x020 => reg_rirqt:       ReadWrite<u32>),
+        (0x024 => reg_ctrl:        WriteOnly<u32>),
+        (0x028 => @END),
+    }
 }
 
 pub struct Mailbox {
     regs: StaticRef<MailboxRegisters>,
-    plic_irq_hiwater: isize,
-    plic_irq_lowater: isize,
+    plic_wtirq: u32,
+    plic_rtirq: u32,
+    plic_eirq: u32,
 }
 
-pub const MAILBOX0: Mailbox = Mailbox {
-    regs: unsafe { StaticRef::new(MAILBOX0_BASE as *mut MailboxRegisters) },
-    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_hiwater: MAILBOX1_HIWATER_IRQ,
-    plic_irq_lowater: MAILBOX1_LOWATER_IRQ,
+pub const MAILBOX: Mailbox = Mailbox {
+    regs: unsafe { StaticRef::new(MAILBOX_BASE as *mut MailboxRegisters) },
+    plic_wtirq: MAILBOX_WTIRQ,
+    plic_rtirq: MAILBOX_RTIRQ,
+    plic_eirq: MAILBOX_EIRQ,
 };
 
 // 32-bit-word bitfield helpers for the PLIC's irq enable lines.
@@ -76,74 +77,61 @@
 }
 
 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);
+    // Synchronously send a message. Blocks the caller if there's no room in the
+    // outbox.
+    pub fn send_message_sync(&self, message: &[u32]) {
         for i in 0..message.len() {
-            self.wait_irq_lowater();
-            self.regs.reg_write.set(message[i]);
+            // NOTE: The spec for the TLUL mailbox says that the write interrupt
+            // fires when the FIFO is _above_ the threshold, which is useless
+            // for us as we need to wait for it to fall _below_ a threshold.
+            // So, we have to busy-wait here, which is slightly annoying.
+            while (self.regs.reg_status.get() & STATUS_BIT_FULL) != 0 {}
+            self.regs.reg_mboxw.set(message[i]);
         }
-        self.regs.reg_ienable.set(0);
-        self.regs.reg_lowater.set(0);
     }
 
-    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.wait_irq_hiwater();
-            message[i] = self.regs.reg_read.get();
+    // Synchronously wait on a message to arrive. Blocks the caller if no
+    // message is in the inbox.
+
+    pub fn wait_recv_sync(&self) {
+        // Set the mailbox to fire the read interrupt when there's more than
+        // zero items in it and enable the corresponding IRQ line in the PLIC so
+        // the interrupt will make it through to the CPU.
+        self.regs.reg_rirqt.set(0);
+        self.regs.reg_intr_enable.set(INTR_ENABLE_BIT_RTIRQ);
+
+        unsafe {
+            set_bit(plic::PLIC_EN0, self.plic_rtirq as isize);
         }
-        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
-    // between the 'if (*flag == 0)' and 'asm("wfi")' statements, we could end up
-    // waiting forever for an interrupt that had already arrived. To prevent that,
-    // we have to globally disable interrupts around those statements. Once
-    // an interrupt has been triggered, 'wfi' will continue and the isr will
-    // execute immediately after global interrupts are re-enabled.
-
-    unsafe fn wait_irq_hiwater(&self) {
-        while (self.regs.reg_status.get() & MAILBOX_STATUS_HIWATER) == 0 {
-            clear_mstatus_bits(MIE_BIT | SIE_BIT);
-            set_bit(plic::PLIC_EN0, self.plic_irq_hiwater);
-            if (self.regs.reg_status.get() & MAILBOX_STATUS_HIWATER) == 0 {
+        // Wait for the read interrupt to fire.
+        while (self.regs.reg_intr_state.get() & INTR_STATE_BIT_RTIRQ) == 0 {
+            unsafe {
                 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);
+        // NOTE: We don't need to deal with the PLIC claim/complete registers here
+        // as we're disabling the interrupt immediately after it arrives and before
+        // any other bit of code has a chance to claim it.
+
+        // Turn the interrupt and IRQ line back off.
+        unsafe {
+            clear_bit(plic::PLIC_EN0, self.plic_rtirq as isize);
+        }
+        self.regs.reg_intr_enable.set(0);
+
+        // Ack it in the mailbox so it doesn't re-fire later.
+        self.regs.reg_intr_state.set(INTR_STATE_BIT_RTIRQ);
     }
 
-    unsafe fn wait_irq_lowater(&self) {
-        while (self.regs.reg_status.get() & MAILBOX_STATUS_LOWATER) == 0 {
-            clear_mstatus_bits(MIE_BIT | SIE_BIT);
-            set_bit(plic::PLIC_EN0, self.plic_irq_lowater);
-            if (self.regs.reg_status.get() & MAILBOX_STATUS_LOWATER) == 0 {
-                asm!("wfi");
+    // Synchronously receive a message. Blocks the caller if no message is in
+    // the inbox.
+    pub unsafe fn recv_message_sync(&self, message: &mut [u32]) {
+        for i in 0..message.len() {
+            while (self.regs.reg_status.get() & STATUS_BIT_EMPTY) != 0 {
+                self.wait_recv_sync();
             }
-            clear_bit(plic::PLIC_EN0, self.plic_irq_lowater);
-            set_mstatus_bits(MIE_BIT | SIE_BIT);
+            message[i] = self.regs.reg_mboxr.get();
         }
-        self.regs.reg_istate.set(IRQ_LOWATER);
     }
 }
diff --git a/utils/src/lib.rs b/utils/src/lib.rs
index 546bbb9..d0b0179 100644
--- a/utils/src/lib.rs
+++ b/utils/src/lib.rs
@@ -62,15 +62,16 @@
             transmute(sel4_pend - elf_loader::elf_phys_min(capdl_segments)),
             transmute((*capdl_elf).e_entry),
         ];
-        matcha_hal::mailbox::MAILBOX1.send_message(&message);
+        matcha_hal::mailbox::MAILBOX.send_message_sync(&message);
         dprintf!("seL4 boot message posted\n");
 
         SMC_CONTROL_BLOCK.write_volatile(entry_point);
 
-        dprintf!("SMC started, waiting on mailbox to clear\n");
+        dprintf!("SMC started, waiting on ACK\n");
 
-        matcha_hal::mailbox::MAILBOX1.wait_lowater(0);
+        let mut reply : [u32;1] = [0];
+        matcha_hal::mailbox::MAILBOX.recv_message_sync(&mut reply);
 
-        dprintf!("Mailbox cleared\n");
+        dprintf!("ACK = 0x{:08X} received, SMC is starting.\n", reply[0]);
     }
 }