Résumé: Andrew Helwer

Software engineer with over a decade of professional experience. Particularly effective when working with distributed systems and formal methods - especially TLA⁺ or Z3. Currently operating as an independent contractor, open to remote contracts or longer-term commitments on interesting projects. Intensive side-interests in quantum computing and formalization of mathematics. Enjoys climbing, submission grappling, and mushroom foraging outside of work!

Located in Atlanta, Georgia, USA. Canadian citizen with permanent residency status in the USA. For contact, email consulting@disjunctive.llc or message me on LinkedIn.


BSc in Computer Science, University of Calgary, Calgary, AB, Canada

Graduated June 2014


Programming languages: Rust, Python, C#, Java, C++, C, Golang

Tools: Kubernetes, Azure, Continuous Integration, Git, Linux, Debuggers, Vim

Formal Methods: TLA⁺, Z3, Lean

Work History

Independent Contractor, Disjunctive LLC

July 28th 2020 - Current (3 years) Atlanta, GA, USA

Developed an error trace replay feature for the TLA⁺ tools. Wrote a TLA⁺ spec of a distributed real-time order management system for a finance company in NYC. Created a TLA⁺ tree-sitter grammar. Used the Z3 theorem prover to analyze role-based access control rules for Teleport, Inc. Wrote a TLA⁺ unicode formatter in Rust. Added CI validation scripting to the tlaplus/examples repo.

Software Engineer II, Microsoft Quantum

May 1st, 2019 - July 28th 2020 (2.25 years) Redmond, WA, USA

Created a popular quantum computing lecture garnering over two million views. Developed tools & services with Kubernetes and F# supporting physicists in the lab as they attempted to reliably manufacture nanowires.

Software Engineer II, Microsoft Azure Networking

May 1st, 2017 - April 30th, 2019 (2 years) Redmond, WA, USA

Designed & implemented a distributed snapshot coordination protocol using formal specification in TLA⁺. Decreased memory footprint of Azure DNS database backend. Worked on automating router configuration updates.

Software Engineer, Microsoft Azure Compute

May 17th, 2014 - April 30th, 2017 (3 years) Redmond, WA, USA

Automated the creation of new Azure regions, datacenters, and clusters using C++, C#, and PowerShell. Identified $8 million in annual data storage cost savings, and personally implemented over $1 million of those savings. Used the Z3 theorem prover to validate a firewall rule modernization effort.

Software Engineer Intern, Microsoft Azure

May 6th, 2013 - July 26th, 2013 (3 months) Redmond, WA, USA

Created a real-time production diagnostic service for internal use by developers in the Microsoft Azure Datacenter Manager team.

Software Developer Intern, Acceleware

May 2nd, 2011 - August 29th, 2012 (16 months) Calgary, AB, Canada

Developed high-performance scientific computing software targeting GPUs. Projects included simulation of electromagnetic waves with the finite-difference time-domain (FDTD) method, CT scan reconstruction, and antenna design for radio-frequency heating. Used C++, CUDA, MPI, and OpenMP.