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.
Education
BSc in Computer Science, University of Calgary, Calgary, AB, Canada
Graduated June 2014
Skills
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.
Talks
- Semantic Highlighting in TLA⁺ (2021)
- Quantum Computing for Computer Scientists (2017)
- The Paxos Protocol (2016)