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. Also competent at working with parsers & interpreters. Currently operating as an independent contractor, open to remote contracts or longer-term commitments on interesting projects. Enjoys mushroom foraging, birdwatching, and Brazilian Jiu-Jitsu outside of work!
Located in Seattle, Washington, USA. Dual Canadian/American citizenship. For contact, email consulting@disjunctive.llc or message me on LinkedIn.
Education
BSc in Computer Science, University of Calgary, Calgary, AB, Canada
Graduated June 2014
Skills
Programming languages: OCaml, Rust, Python, Java, C++, C, C#, Go, CUDA
Tools: CI, Git, Linux, Nix, Vim, Parsers, Debuggers, Kubernetes, Azure
Formal Methods: TLA⁺, Z3, Lean
Work History
TLA⁺ Core Developer, TLA⁺ Foundation Grant
January 2024 - Current (~2 years), Remote
Developed several large test corpora for the TLA⁺ language standard, validating conformance of all existing tooling. Wrote a how-to guide for creating a TLA⁺ model checker from scratch. Added support for parsing Unicode math symbols in TLA⁺. Developed the tlaplus/examples repo into a large real-world test resource for TLA⁺ language tooling. Wrote a TLA⁺ unicode formatter in Rust. Created a TLA⁺ tree-sitter grammar.
Independent Contractor, Disjunctive
July 28th 2020 - Current (~5 years), Remote
Used TLA⁺ to help design a vector database configuration update protocol for a company in San Francisco. Used the Z3 theorem prover to analyze role-based access control rules for Teleport, Inc. Wrote a TLA⁺ spec of a distributed real-time order management system for a finance company in New York City.
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.