Hi, my name is Hays. I also go by Carson. I currently work in the Prescience Lab, led by Professor Peter Dinda.

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

The following projects are my current focus:

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

• Renert: A self-generating libOS for kernel-bypass runtimes, 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 (~$65k USD as of 11/01/24).

  • This includes various standalone subprojects:

    • WASMwand: An application using WAI bindgen code for integration with specialized microkernels, such as Nautilus

    • MLIRacle: A verified MLIR dialect encoding various elliptic curve forms

    • Demo of improvement of the EEVDF scheduler on Linux via sched_ext/eBPF

    • A proof-supported MVP relating to the MCSP. A whitepaper will be released June 1st, 2025.

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 verified Vector/BF16 extension support in 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.

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: 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, C23, Koka, Prolog, F#, Julia, and Janet.

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

I like water polo, competitive poker, and fashion design in my free time. If you’re interested in working on something together, contact me via email: hays <at> surmeier <dot> us.

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

• “I always finish my side projects.” - Me