I work at Arm Research.

My interests include privacy, confidential computing, formal methods, trusted execution environments, operating systems, programming languages, and reverse engineering.

Please feel free to reach out using any of the links above.

Resume (pdf)

Papers and talks

seL4 + TrustZone: Spanning both worlds
seL4 Summit 2020 – Nick Spinale

Newly reducible polynomial iterates
International Journal of Number Theory – Peter Illig, Rafe Jones, Eli Orvis, Yukihiko Segawa, Nick Spinale

Selected open source activity

seL4 - I'm an active contributor to seL4, the formally verified microkernel. My contributions span the kernel itself and CapDL.

Isabelle + Nix - The Isabelle developers suggested that trying to repackage, let alone port, Isabelle would be insane: [1] [2]. Nix provides a realistic and satisfying means to such a port. To prove it, I've used Nix to port Isabelle to Arm. This port has just recently become relevant due to the MacOS transition to Arm.

Nixpkgs - I'm an active contributor to the Nix packages collection.

Selected professional experience

Arm Research | Senior Research Engineer
October 2018 – Present | Cambridge, UK

Google | Software Engineering Intern
June – September 2017 | Mountain View, CA

Carve Systems, LLC | HackNY Fellow + Intern
June – December 2016 | New York, NY


Carleton College | Mathematics and Computer Science
Sep 2014 – June 2018 | Northfield, MN


David Pollatsek Prize in Computer Science
2018 – Carleton College

Phi Beta Kappa
2018 – Carleton College

HackNY Fellow
2016 – hackNY

United States Presidential Scholar
2014 – United States Department of Education

Academic services

(Session chair) Morello: Investigating hardware capabilities in the Arm architecture
Arm Research Summit 2020 – Richard Grisenthwaite (Chief Architect at Arm), Robert Watson (University of Cambridge), and Peter Sewell (University of Cambridge)

Selected independent projects

hs-arm - ARM (dis)assembler and analyzer Haskell library generated from the machine-readable ARMv8.3-A specification.

Malice - Haskell framework that provides abstractions and protocol-specific attacks for intercepting and modifying network traffic. It leverages the power of Haskell’s type system to define an embedded DSL for describing the actions of Eve and Mallory. In effect, it allows a person in the middle to write code that is as close to pure evil as possible.

pyxendbg - GDB server for virtual machine introspection under Xen. Inspired by xendbg, but with Arm in mind. Designed for debugging paravirtutalized unikernel guests.

regl - Haskell library for applicative-style regular expressions. Features uncommon yet useful primitives such as regular expression complement and disjunction. Based on regular expression derivatives.

kgo - kexec implemented in pure Go, with some extra flexibility. Designed to boot a type-1 hypervisor such as Xen or Hafnium, with LinuxBoot in mind.

routor - Tor controller that allows circuit paths to be chosen on a stream-by-stream basis.

wmonad - A set of Haskell libraries encapsulating interaction with the X11 server, enabling the expression of pure X11 logic.