corpus.blog
56,966 blogs · [ { "id": "01a0e2e2-29b7-738c-9627-eb307d6dbbf0", "title": "Can we have reachability properties in TLA⁺?", "url": "https://ahelwer.ca/post/2026-09-26-reachability/", "published_at": "2026-09-26T00:00:00+00:00" }, { "id": "01a0d50c-2f53-703f-8439-57df0ac49245", "title": "Textbook review: Is Parallel Programming Hard, And, If So, What Can You Do About It?", "url": "https://ahelwer.ca/post/2026-09-21-concurrency-textbook/", "published_at": "2026-09-21T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6935d253", "title": "The changing role of finite-state model checking", "url": "https://ahelwer.ca/post/2026-08-24-finite-state-future/", "published_at": "2026-08-24T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab69fec1a8", "title": "Laptops all have built-in security tokens these days", "url": "https://ahelwer.ca/post/2026-05-08-builtin-u2f/", "published_at": "2026-05-08T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6a949ad2", "title": "Let go of StackOverflow; communities must take ownership", "url": "https://ahelwer.ca/post/2025-11-25-stackoverflow/", "published_at": "2025-11-25T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6ad72a35", "title": "A supposedly worthwhile contract I'll never do again", "url": "https://ahelwer.ca/post/2025-07-04-tla-contracts/", "published_at": "2025-07-04T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6affcbd2", "title": "The current state of TLA⁺ development", "url": "https://ahelwer.ca/post/2025-05-15-tla-dev-status/", "published_at": "2025-05-15T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6be01a9e", "title": "TLA⁺ is more than a DSL for breadth-first search", "url": "https://ahelwer.ca/post/2024-09-18-tla-bfs-dsl/", "published_at": "2024-09-18T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6c81081b", "title": "TLA⁺ Unicode support", "url": "https://ahelwer.ca/post/2024-05-28-tla-unicode/", "published_at": "2024-05-28T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6cf03b3e", "title": "Wrangling monotonic systems in TLA⁺", "url": "https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/", "published_at": "2023-11-01T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6d7e2d17", "title": "FOSS I Love", "url": "https://ahelwer.ca/post/2023-04-29-sunshine-moonlight/", "published_at": "2023-04-29T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6d916c82", "title": "Inlining SVGs for Dark Mode", "url": "https://ahelwer.ca/post/2023-04-06-dark-mode/", "published_at": "2023-04-06T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6e1e16e1", "title": "Using TLA⁺ at Work", "url": "https://ahelwer.ca/post/2023-04-05-checkpoint-coordination/", "published_at": "2023-04-05T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6ecf8346", "title": "Pseudocode Showdown", "url": "https://ahelwer.ca/post/2023-03-30-pseudocode/", "published_at": "2023-03-30T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6f445f0f", "title": "Google Groups has been left to die", "url": "https://ahelwer.ca/post/2023-03-08-google-groups/", "published_at": "2023-03-08T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6f4ff5e8", "title": "Can sanitizers find the two bugs I wrote in C++?", "url": "https://ahelwer.ca/post/2023-02-07-cpp-bugs-sanitized/", "published_at": "2023-02-07T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab6ff7348c", "title": "Two C++ bugs I wrote", "url": "https://ahelwer.ca/post/2023-02-04-cpp-bugs/", "published_at": "2023-02-04T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab70cb8bb1", "title": "Writing a TLA⁺ tree-sitter grammar", "url": "https://ahelwer.ca/post/2023-01-11-tree-sitter-tlaplus/", "published_at": "2023-01-11T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab70e2b90d", "title": "What's the difference between a computer and a rock?", "url": "https://ahelwer.ca/post/2022-10-19-defining-computation/", "published_at": "2022-10-19T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab7190465c", "title": "The Missing Prelude to The Little Typer's Trickiest Chapter", "url": "https://ahelwer.ca/post/2022-10-13-little-typer-ch9/", "published_at": "2022-10-13T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab7258bfe3", "title": "Regexes in the Z3 Theorem Prover", "url": "https://ahelwer.ca/post/2022-01-19-z3-rbac/", "published_at": "2022-01-19T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab729170c2", "title": "Two pictures of quantum computation", "url": "https://ahelwer.ca/post/2020-12-06-sum-over-paths/", "published_at": "2020-12-10T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab72baece2", "title": "How do you reason about a probabilistic distributed system?", "url": "https://ahelwer.ca/post/2020-09-11-probabilistic-distsys/", "published_at": "2020-09-11T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab72fc8e6e", "title": "Meditation", "url": "https://ahelwer.ca/post/2020-08-29-meditation/", "published_at": "2020-08-29T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab73281a00", "title": "Taking my home work setup seriously", "url": "https://ahelwer.ca/post/2020-08-14-home-ergonomics/", "published_at": "2020-08-14T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab732a0b9b", "title": "Doing a math assignment with the Lean theorem prover", "url": "https://ahelwer.ca/post/2020-04-05-lean-assignment/", "published_at": "2020-04-05T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab7371efa2", "title": "Simulating physical reality with a quantum computer", "url": "https://ahelwer.ca/post/2019-12-21-quantum-chemistry/", "published_at": "2019-12-21T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab7400e8b0", "title": "Walking the faster-than-light tightrope", "url": "https://ahelwer.ca/post/2018-12-07-chsh/", "published_at": "2018-12-07T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab74118323", "title": "Checking Firewall Equivalence with Z3", "url": "https://ahelwer.ca/post/2018-02-13-z3-firewall/", "published_at": "2018-02-13T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab74cfb852", "title": "Formal Verification, Casually Explained", "url": "https://ahelwer.ca/post/2018-02-12-formal-verification/", "published_at": "2018-02-12T00:00:00+00:00" }, { "id": "01a08721-59ab-73be-b067-f6ab75be2cba", "title": "Andrew Helwer", "url": "https://ahelwer.ca/resume/", "published_at": null } ] posts Claim your blog
Back to ahelwer.ca
Blog · corpus.blog/blogs/ahelwer.ca/posts

ahelwer.ca

ahelwer.ca

2026

Can we have reachability properties in TLA⁺?original ↗
26 Sept 2026
Textbook review: Is Parallel Programming Hard, And, If So, What Can You Do About It?original ↗
21 Sept 2026
The changing role of finite-state model checkingoriginal ↗
24 Aug 2026
Laptops all have built-in security tokens these daysoriginal ↗
8 May 2026

2025

Let go of StackOverflow; communities must take ownershiporiginal ↗
25 Nov 2025
A supposedly worthwhile contract I'll never do againoriginal ↗
4 Jul 2025
The current state of TLA⁺ developmentoriginal ↗
15 May 2025

2024

TLA⁺ is more than a DSL for breadth-first searchoriginal ↗
18 Sept 2024
TLA⁺ Unicode supportoriginal ↗
28 May 2024

2023

Wrangling monotonic systems in TLA⁺original ↗
1 Nov 2023
FOSS I Loveoriginal ↗
29 Apr 2023
Inlining SVGs for Dark Modeoriginal ↗
6 Apr 2023
Using TLA⁺ at Workoriginal ↗
5 Apr 2023
Pseudocode Showdownoriginal ↗
30 Mar 2023
Google Groups has been left to dieoriginal ↗
8 Mar 2023
Can sanitizers find the two bugs I wrote in C++?original ↗
7 Feb 2023
Two C++ bugs I wroteoriginal ↗
4 Feb 2023
Writing a TLA⁺ tree-sitter grammaroriginal ↗
11 Jan 2023

2022

What's the difference between a computer and a rock?original ↗
19 Oct 2022
The Missing Prelude to The Little Typer's Trickiest Chapteroriginal ↗
13 Oct 2022
Regexes in the Z3 Theorem Proveroriginal ↗
19 Jan 2022

2020

Two pictures of quantum computationoriginal ↗
10 Dec 2020
How do you reason about a probabilistic distributed system?original ↗
11 Sept 2020
Meditationoriginal ↗
29 Aug 2020
Taking my home work setup seriouslyoriginal ↗
14 Aug 2020
Doing a math assignment with the Lean theorem proveroriginal ↗
5 Apr 2020

2019

Simulating physical reality with a quantum computeroriginal ↗
21 Dec 2019

2018

Walking the faster-than-light tightropeoriginal ↗
7 Dec 2018
Checking Firewall Equivalence with Z3original ↗
13 Feb 2018
Formal Verification, Casually Explainedoriginal ↗
12 Feb 2018

Undated

Andrew Helweroriginal ↗
—