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!
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
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.