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 the formalization of mathematics. Enjoys mushroom foraging, birdwatching, and BJJ outside of work!

Located in Atlanta, Georgia, 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: Rust, Python, Java, C++, C, C#, Golang

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

Formal Methods: TLA⁺, Z3, Lean

Work History

Independent Contractor, Disjunctive Consulting LLC

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

Professional contracts: 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. Developed an error trace replay feature for the TLA⁺ Java tools.

FOSS contributions: Added support for parsing Unicode math symbols in TLA⁺. Developed a unified TLA⁺ syntax test corpus, massively improving testing of several TLA⁺ tools. Added CI validation to the tlaplus/examples repo and added many modules & models, turning it into a valuable test corpus for new language tooling. Wrote a TLA⁺ unicode formatter in Rust. Created a TLA⁺ tree-sitter grammar.

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.

Talks