Hi, my name is Carson. I currently work in the Prescience Lab, led by Professor Peter Dinda. I’m a dual major in computer science and mathematics at Northwestern; I expect to graduate by June 2025.

• My main research interests are operating systems, software/hardware formal verification, cryptography, algebraic geometry, and homotopy type theory.

The following projects are my current focus:

• Tortoise (Senior Thesis): a distributed, geolocation-based model of differential privacy, implemented using a novel application of moduli spaces, ECC, and UWB.

• WASMwand: A libOS and WASM runtime, based on HoTT-derived capability security. Most notably inspired by Mirage OS, Demikernel, Genode Framework, and seL4.

  • This work in particular is entirely self-funded (appox. $65k USD as of 11/24).

  • A verified MVP relating to the MCSP as well as work improving the EEVDF scheduler on Linux via sched_ext/eBPF will be released June 1st, 2025; email me at ${first_name}@surmeier.us for more information.

I currently contribute to the following:

• Constellation: NU and CMU project group aimed at developing full software and hardware stack for frictionless heterogeneous parallelism.

• Village: compiler for NESL/VCODE to LLVM-IR. My current work is adding verification passes to custom RISC-V cores with Clash HDL and SymbiYosys.

Some toy projects I’m working on:

• Beet Takeshi: a provably perfect decompilation and TAS of the NES game Takeshi no Chōsenjō.

• PokerBowl: FOSS Texas Hold ‘em site similar to lichess, with a client-side GTO solver. Built with Servant, Reflex, and WebGPU.

• ECIR: A MLIR dialect for efficiently encoding elliptic curve forms. Loosely related to HEIR.

Notable previous contributions:

• CARAT KOP: memory guards for Linux kernel modules. A paper on this topic was accepted to ROSS 2023 as of September 8th, 2023.

• Privacy Backplane: NU, UMich, and Pitt project group focused on enabling individualized privacy policies in TEE-enabled IoT environments, such as cashierless stores. My work was centered around prototyping the distributed backend with libp2p.

• Nautilus Microkernel, core member of the team responsible for the RISC-V and ARMv8-A port.

• TrackFM: a transparent, and user level, far memory management system, developed at Hexsa Lab in IIT. Work was focused on LLVM integration.

• Linux kernel projects: Mesa VirGL, KVM

Language knowledge:

• I’m highly proficient in Haskell, C, Koka, Rust, Isabelle, Julia/OSCAR.jl, and Janet.

• I have high familiarity with and am actively learning TLA+, Rzk, F*/Low*, Nix/Dhall, Sail DSL, Lean 4, and RISC-V Assembly.

I like jiu-jitsu and competitive poker in my free time. If you’re interested in working on something together, contact me at ${first_name}@surmeier.us.

“The valor that struggles is better than the weakness that endures.” - Hegel