Independent software engineering consultant with over a decade of professional experience. Previously worked at Acceleware, Microsoft Azure Compute, Microsoft Azure Networking, and Microsoft Quantum. BSc in Computer Science from the University of Calgary. From Canada, currently based out of Atlanta, GA, USA. TLA⁺ enthusiast!

Interested in hiring me for a contract? Contact me on LinkedIn or email consulting@disjunctive.llc. Work playing to my skills includes:

  • Formally specifying & model-checking your system with TLA⁺ [1] [2]
  • Formally proving the correctness of your system [1] [2]
  • Assisting in the design of your distributed system or protocol [1]
  • Analyzing your probabilistic system or protocol with PRISM [1]
  • Writing tricky distributed systems code for your system’s backend [1]
  • Validating your system’s implementation with model-based testing
  • Analyzing your access control system with the Z3 theorem prover [1] [2]
  • Writing a tree-sitter grammar for your domain-specific language [1]
  • Education in technical quantum computing concepts [1] [2] [3] [4]
  • General development work on formal methods tools themselves [1]

I have experience with C++, Java, C#, Rust, Golang, Python, and Kubernetes. See my full résumé here.

Email ahelwer@protonmail.com for personal correspondence. I’m always happy to answer questions about my interests, especially quantum computing!

Outside of work I’m an avid climber; find tales & photos of my adventures at outdoors.ahelwer.ca.

All content on this website is licensed under CC-BY-SA 4.0.

Walking the faster-than-light tightrope

Quantum entanglement and the CHSH game

Walking the faster-than-light tightrope

 Posted on December 7, 2018  |  Andrew Helwer

Measurement and signaling in the nonlocal world Popular understanding of quantum mechanics usually focuses on three learning objectives: At small scales, particle properties (position, momentum, spin, etc.) are in superposition - they don’t have a definite value, but instead are “smeared” across multiple possible values. Measuring a superposed particle property makes it collapse probabilistically to a specific value. We don’t simply discover the property’s pre-existing value; rather the property is forced to take on a definite value by the act of measurement. [Read More]
quantum computing 

Checking Firewall Equivalence with Z3

Checking Firewall Equivalence with Z3

 Posted on February 13, 2018  |  Andrew Helwer

Lessons I’ve learned from software engineering are uniformly cynical: Abstraction almost always fails; you can’t build something on top of a system without understanding how that system works. Bleeding-edge methods are a recipe for disaster Everything good is hype and you’ll only ever get a small fraction of the utility being promised. Imagine my surprise, then, when the Z3 constraint solver from Microsoft Research effortlessly dispatched the thorniest technical problem I’ve been given in my short professional career. [Read More]
formal methods  smt solvers 

Formal Verification, Casually Explained

Written during an interesting time in my life

Formal Verification, Casually Explained

 Posted on February 12, 2018  |  Andrew Helwer

Why are we here? What guarantees does formal verification provide? This question rests at the apex of a hierarchy of inquiry extending all the way down to how we can know anything at all! What do we mean by software correctness? There are precisely two different ways for a piece of software to be correct: The supreme deity of the universe descends from the heavens and decrees, with all the weight of Objective Truth, that a certain piece of software is correct. [Read More]
formal methods  philosophy