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:

  • Assisting you in formally specifying & model-checking your system with TLA⁺ [1] [2] [3]
  • Assisting in the design of your distributed system or protocol [1]
  • Validating system implementation with model-based testing or trace validation
  • Analyzing your access control system with Z3 [1] [2]
  • Writing a tree-sitter grammar for your domain-specific language [1]
  • General development work on formal methods tools themselves [1] [2]

I have experience with Java, Python, Rust, OCaml, C++, C#, Golang, 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.

A supposedly worthwhile contract I'll never do again

A supposedly worthwhile contract I'll never do again

Here I’ll talk about a type of TLA⁺ contract I’ve worked on a few times, and why it didn’t work out as well as hoped. I’m not trying to torpedo other peoples’ contracts here - I just hope to share this experience so others can structure their TLA⁺ contracts differently, hopefully leading to greater success for both parties and industry usage of TLA⁺ as a whole.

The proposal

The contract proposal goes like this: a client wants to build a distributed system, and has read that TLA⁺ is effective at modeling such things. Conventional wisdom holds that it’s always cheaper to catch bugs earlier in the development pipeline, and what’s earlier than the design stage? However, they don’t have any in-house TLA⁺ knowledge and are unsure about whether they want to invest in training or hiring. Instead, they email me a proposal: could I do a short 1-3 month contract where I specify their system in TLA⁺ for them? The benefits of this setup are generally reasoned as follows:

[Read More]

The current state of TLA⁺ development

The current state of TLA⁺ development

The 2025 TLA⁺ Community Event was held last week on May 4th at McMaster University in Hamilton, Ontario, Canada. It was a satellite event to ETAPS 2025, which I also attended, and plan to write about in the near future. I gave a talk somewhat-hucksterishly titled It’s never been easier to write TLA⁺ tooling! which I will spin into a general account of the state of TLA⁺ development here. The conference talks were all recorded, so if you’d like this blog post in video form you can watch it below:

[Read More]

TLA⁺ is more than a DSL for breadth-first search

TLA⁺ is more than a DSL for breadth-first search

Although it isn’t usually taught that way, a lot of TLA⁺ newcomers develop the understanding that TLA⁺ is just a fancy domain-specific language (DSL) for breadth-first search. If you want to model all possible executions of a concurrent system - so the thinking goes - all you have to do is define:

  1. The set of variables modeling your system
  2. The values of those variables in the initial state(s)
  3. Possible actions changing those variables to generate successor states
  4. Safety invariants you want to be true in every state

The model checker will then use breadth-first search (BFS) to churn through all possible states (& thus execution orders) of your system, validating your invariants. If one of your invariants fails, BFS gives you the shortest execution path reaching that state. It even checks for deadlock by finding states with no possible successor states.

[Read More]

TLA⁺ Unicode support

Learning to work with others in open source

TLA⁺ Unicode support

TLA⁺ was developed by Leslie Lamport, originator of \(\LaTeX\), so it’s unsurprising that TLA⁺ syntax looks pretty \(\LaTeX\)-y. It’s a very mathy language, with much use of symbols like (among others) \A,\E, /\, \/, and \in denoting \(\forall\), \(\exists\), \(\land\), \(\lor\), and \(\in\) respectively. The language tools include a tla2tex command to format TLA⁺ specs into \(\LaTeX\) for integration in research papers. However, research papers are not where I spend the most time looking at TLA⁺. Here’s the tale of how I brought those beautiful symbols into the code editor, and how I learned to work with others in FOSS along the way!

[Read More]

Wrangling monotonic systems in TLA⁺

Tractable modeling of replicated logs & CRDTs

Wrangling monotonic systems in TLA⁺

TLA⁺ sees a lot of use modeling distributed systems. The ability to explore all possible interleavings of events makes concurrency simple to reason about. For this TLA⁺ uses something called finite model-checking, which is really just a breadth-first search through the entire state space. The key here - and this really must be emphasized - is that the model is finite. There can’t be an infinite number of states, or of course the model checker will run forever.

[Read More]

FOSS I Love

Local game streaming with Sunshine and Moonlight

FOSS I Love

Here I’ll write an ode to two closely-linked FOSS projects that have, recently, absolutely floored me with their competence & quality: Sunshine and Moonlight. These are used to stream video games over a (usually local) network. Sunshine is a game streaming server: it runs on your PC as it chugs away doing all the heavy lifting of running the game itself, while Moonlight is a game streaming client that runs on whatever thin hardware exists where you want to play the game! I run Sunshine on my home office workstation and Moonlight on a NVIDIA Shield Android TV connected to a 55" screen in the living room. Some games are just best played on the couch! It’s also important if you have someone you want to share the experience with instead of sequestering yourself alone in your dark Gamer Den.

[Read More]

Inlining SVGs for Dark Mode

Inlining SVGs for Dark Mode

I will here indulge in the traditional practice of using my blog to talk about how I’m using my blog. This page is built with the Hugo static site generator. I recently updated it to use the latest version of the beautifulhugo theme, which unbeknownst to me included a dark mode colorscheme. Recent browsers use the prefers-color-scheme option to automatically choose light or dark mode CSS styles, if the website supports it. And my website did support it, not that I knew it until people started commenting that my syntax-highlighted code blocks were unreadable! I figured out how to toggle light/dark mode in Firefox (ctrl+shift+I to open the inspector pane then click the sun/moon icons), perused my website, and found an even greater problem: my treasured vector diagrams that I put so much time & effort into were completely invisible against a dark background! Here’s a quick post about supporting dark mode on my blog by inlining SVGs and setting their color with the currentColor CSS variable.

[Read More]

Using TLA⁺ at Work

Designing a snapshot coordination system

Using TLA⁺ at Work

Here’s a short report of a time I used TLA⁺ at work, with interesting results. TLA⁺ is a formal specification language that is particularly effective when applied to concurrent & distributed systems. TLA⁺ made it tractable for an ordinary software engineer to reason about a tricky distributed systems problem, and it found a bug introduced by an “optimization” I tried to add (classic). The bug required 12 sequential steps to occur and would not have been uncovered by ordinary testing.

[Read More]

Pseudocode Showdown

Python vs. PlusCal & TLA⁺

Pseudocode Showdown

Last weekend I had a conversation with an undergraduate student new to computer science, who was reading CLRS. “I wish” they said, “that all the pseudocode in my algorithms textbook was just written in Python.” “Ah” I said, “but textbook authors sometimes want their work to endure beyond a decade.” “But Python’s been around for a long time” came the reply, “and it’s very readable, and you can’t execute pseudocode anyway so what’s the harm?”

[Read More]

Google Groups has been left to die

Where should the formal methods community move?

Google Groups has been left to die

An unusual topic for this blog, but worth boosting to a larger audience: Google Groups is dying. Its epitaph is not yet inscribed on the Killed by Google website, but the end is easily seen from here (although it should also be noted its death was called as early as 13 years ago). The deficiencies in Google Groups search, supposedly Google’s forte, have long been noted. Lately though basic features have just stopped working.

[Read More]