diff --git a/KataGdbUserSpaceDebugging.md b/KataGdbUserSpaceDebugging.md
new file mode 100644
index 0000000..a360ee0
--- /dev/null
+++ b/KataGdbUserSpaceDebugging.md
@@ -0,0 +1,123 @@
+# How to Use GDB with Renode to Debug seL4 Threads with Symbols
+
+## High-Level Usage
+
+The method for debugging seL4 threads with Renode is relatively simple, and
+involves the usual suspects of `m simulate-debug` and `kgdb.sh`, but the
+interface through GDB has changed slightly. In general, a debugging session now
+looks like the following:
+
+On one terminal, start an instance of Renode:
+```bash
+source build/setup.sh
+m simulate-debug
+```
+
+Once Renode has started and starts outputting green debug logs, in another
+terminal start up GDB with:
+```bash
+kgdb.sh
+```
+
+At this point, GDB should connect to the running Renode instance started by
+`simulate-debug`, and you'll see something equivalent to the following (output
+is not exact -- symbol reading may differ):
+
+```
+ghost:~/$ kgdb.sh
+Source directories searched: /usr/local/google/home/jtgans/shodan/sw/tock:$cdir:$cwd
+Reading symbols from out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf...
+add symbol table from file "out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf"
+Reading symbols from out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf...
+add symbol table from file "out/matcha/riscv32imc-unknown-none-elf/debug/matcha_platform"
+Reading symbols from out/matcha/riscv32imc-unknown-none-elf/debug/matcha_platform...
+add symbol table from file "out/matcha/riscv32imc-unknown-none-elf/debug/matcha_app"
+Reading symbols from out/matcha/riscv32imc-unknown-none-elf/debug/matcha_app...
+Remote debugging using localhost:3333
+warning: multi-threaded target stopped without sending a thread-id, using first non-exited thread
+0x20007b4a in tock_cells::map_cell::MapCell<kernel::callback::AppId>::is_some<kernel::callback::AppId> (self=0x10005af4 <matcha_platform::reset_handler::BUF>)
+    at /usr/local/google/home/jtgans/shodan/sw/tock/libraries/tock-cells/src/map_cell.rs:47
+47              self.occupied.get()
+(gdb)
+```
+
+At this point, GDB has stopped the simulator, giving you a chance to set
+breakpoints and examine the system.
+
+`kgdb.sh` will automatically load symbols on the seL4 side, based upon their
+thread names, so there is no need to manually find the associated symbol file
+and load it with the correct offsets. It may be necessary to switch symbol
+tables, which can easily be done using `sel4 switch-symbols <threadname>`, which
+will automatically load them with the appropriate offsets.
+
+In this environment, there are two sets of breakpoints that can be used:
+standard gdb `break`-style breakpoints, and renode-side `sel4 break`
+breakpoints. The former work within the currently executing thread and can be
+used for "local" breaks inside of a thread, whereas the latter can be set in any
+thread that was previously discovered by the Renode extension.
+
+Once you've setup your breakpoints using `sel4 break`, you'll need to tell
+Renode to enable breakpoints as well with `sel4 breakpoints-enabled True`, and
+then `continue`. For example, consider this debugging session:
+
+```
+<assuming cpu1 is halted and gdb is waiting at a prompt>
+
+(gdb) # Wait until 'rootserver' thread is set up in seL4
+(gdb) sel4 wait-for-thread rootserver
+
+(gdb) # rootserver thread is now the symbol "main" in the thread/program, so we
+(gdb) # can break on stopped and associated symbols are loaded.
+(gdb) sel4 break rootserver main
+
+(gdb) # Enable extension breakpoints (it's disabled by default as it's pretty
+(gdb) # performance-heavy as Renode has to break on every context-switch)
+(gdb) sel4 breakpoints-enabled True
+(gdb) c
+
+(gdb) # We are in capdl-loader main() function, disable extension breakpoints
+(gdb) sel4 breakpoints-enabled False
+
+(gdb) # As we are in capdl-loader thread and proper symbols are loaded, all commands
+(gdb) # like break are working correctly
+(gdb) b init_system
+(gdb) c
+```
+
+## Theory of Operation
+
+The kgdb.sh / Renode symbol lookup mechanism is composed of two parts: a custom
+Renode extension in `sim/config/shodan_infrastructure/seL4Extensions.cs` and a
+custom GDB extension in `sim/config/gdbscript.py`. `kgdb.sh` is a simple bash
+script that starts GDB and connects to the appropriate remote with the extension
+loaded.
+
+The Renode extension tracks the VSpace setup for each thread and translates
+virtual addresses to physical addresses. Without this work symbols may be
+incorrectly resolved because every VSpace memory range starts at 0.
+
+In addition, the extension provides commands to Renode to add debugging hooks to
+an execution, all prefixed with the subcommand `seL4` (case matters at the
+Renode prompt!). In our simulation config, Renode is configured to start the
+seL4 extension on cpu1 using the `cpu1 CreateseL4` command.
+
+The GDB extension provides a matching set of wrappers via the `sel4` command
+prefix to examine the simulator state and take a look at threads in the system.
+
+Both extensions provide built in help at their respective command lines, but
+suffice it to say, the GDB extension is essentially just an automation mechanism
+to load in symbols for the current thread context from disk when the Renode
+extension detects a context switch.
+
+During debugging, not all symbols will be loaded in GDB at the start, so it can
+be helpful to use `sel4 wait-for-thread <threadname>` to tell Renode to break
+execution upon entry of the given thread. When the break occurs, Renode will
+instruct GDB to load the correct symbol table, and then symbols can be resolved
+for later breakpoints, etc.
+
+To set a breakpoint for a thread that is not the current context, use the `sel4
+break <threadname> <symbol>` command. This will instruct Renode to load the
+appropriate symbol table and break at the right place once that thread is
+running. If, however, you need to set a breakpoint in the current thread
+context, it's fine to use `break` as normal, since the symbols for the current
+thread should be loaded.