Hacker News Reader

It does not spit out C. TLA+ is aimed at the design/specification level, not the implementation level. You would have to take the information learned from the model checker or proof system (or even just the act of constructing the model can reveal problems) and change your program to address any discovered issues.

The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec.

Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.

In practice it's fuzzy but TLA+ is meant for checking your thinking not your code as per se