I am a researcher at VMware Research. I presently focus on applying software verification to distributed systems protocols and implementations, with a particular interest in making verification into a practical engineering tool. My primary project is VeriBetrFS, a high-performance verified filesystem. My office is in Bellevue, WA.
I am an affiliate professor at the University of Washington's Paul G. Allen School of Computer Science & Engineering. I co-instructed CSE 552 at the University of Washington in Spring 2019.
Until 2018, built distributed systems at Google, mostly on the Slicer project, a state-aware sharding service.
Prior to 2015, I was a distributed systems researcher at Microsoft Research. I applied formal verification to practical systems. We built Ironclad Apps, which are single-node security-sensitive applications, proven to meet a given functional spec, with verification of every assembly instruction. We followed that with IronFleet, distributed systems of cooperating nodes proven to meet a function spec, with verification down to imperative source code.
I also helped create Flat Datacenter Storage, a scalable high performance data center file system that claimed the 2012 Minute Sort record.
My first project at MSR was the Farsite distributed filesystem. I focused on practical techniques for managing concurrency in distributed systems programming, including using formal specification to design the distributed directory service for FARSITE, which must be simultaneously scalable, consistent, and Byzantine-fault-isolating [OSDI2006], using atomic actions as a practical technique to simplify the management of local concurrency, and clarifying the relationship between cooperative threads and event-driven code [Usenix2002].
After grad school, I spent a year at Consystant, a startup company in Kirkland, studying and modeling language semantics.
I developed my dissertation at Dartmouth working with David Kotz on distributed naming and security. I extended a formal system to model the transitive delegations of the Simple Public Key Infrastructure (SPKI). The result is a system that can reason about authorization across administrative boundaries, without a centralized notion of a domain that contains a list of people or principals. I also spent far too much time in the robotics lab, diddling with hardware and mapping algorithms.