Jon Howell

Jon Howell
Software Engineer
Distributed Systems


My personal page is I can be reached at jonh(dot)msrref[at]

I am a software engineer building distributed systems at Google. My current project is Slicer, 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 developed a new model of client execution called Embassies that shifts responsibility for application security and management from end users to application vendors. Find the code at Codeplex.

I also helped create Flat Datacenter Storage, a scalable high performance data center file system that claimed the 2012 Minute Sort record.

I co-developed Asirra and InkblotPasswords. I also co-developed the MapCruncher tool for importing map content onto the web; it now ships from Microsoft.

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.

Jon flies airplanes, bicycles, plays puzzlehunt, and has built a rocketship treehouse.

Thu Feb 15 22:23:39 PST 2018