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. Has 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. I am a 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++, Golang

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

Formal Methods: TLA⁺, Z3, Lean

Work History

Independent Contractor, Disjunctive LLC

July 28th 2020 - Current (2.5 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 Enginer 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 Engineeer 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.