So can it spit out C or something? Or something to actually perform the algorithm? Or are you expected to manually translate back and forth between your model specification and your code?
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.
