8 engineers on Hacker News describe using TLA+ first-hand: 4 endorse it, 1 regret it, 1 are mixed.
“I have been using TLA+ for writing specifications of distributed algorithms... The value of temporal properties in TLA+ is overrated.”
mixed · personal · 6 yr · igornotarobot · 2025-12-17 · source ↗ · wrong label?“We've been using TLA+ at Amazon for a long time”
endorse · production · mjb · 2020-12-15 · source ↗ · wrong label?“TLA+ can be very useful outside distributed systems. For example, I'm currently working on a virtualization-related low-level systems paper”
endorse · personal · mjb · 2020-12-15 · source ↗ · wrong label?“We use TLA+... I expect that if we had to go back and do it all over again we'd have selected something else. The specification language has some annoying warts”
regret · production · im_down_w_otp · 2019-11-29 · source ↗ · wrong label?“Correctness has been proven with TLA+ https://github.com/pingcap/tla-plus”
endorse · production · morgo · 2018-12-04 · source ↗ · wrong label?“I enjoyed every minute of it! ... it's easy to learn and you can get productive very fast.”
endorse · personal · pron · 2016-12-14 · source ↗ · wrong label?“I just bite the bullet and go to full model checking with something like Alloy or TLA+.”
neutral · production · erichocean · 2023-12-06 · source ↗ · wrong label?“I've actually built something like this for TLA+ and C#, which I call Kayfabe.”
neutral · personal · sterlind · 2020-02-23 · source ↗ · wrong label?