Sure, but not all of us are building products at the scale of Amazon and Microsoft. When you're shipping something like DynamoDB, the argument for TLA+ is obvious. What's harder to come across are the people finding ways to make use of technologies like this on a smaller scale, and I think that's one place where Hacker News really shines as a way of connecting people.

At least personally, working at a small and understaffed startup, I'm not always going to find the time to put together big case studies on interesting things I do, but it's a lot easier to share a sentence or two on a casual Hacker News thread. I wouldn't be surprised if it's the same for other people.

That's not what was asked for. However I understand where you're coming from and am with you. I wish I had the chance to use TLA, or all the other goodies that seem ruled out by the results now and damn the bugs! mindset.

Fair :) My question was meant with more of a conversational slant than an objective one, but I can see how that tone gets lost over text. i.e. It's obvious that some people use TLA+, but I'm interested in what specifically the people here are using it for.