I think this spec tries to do two things, only one of which fits in with the purpose of TLA+. I think this is caused by some ambiguity regarding the source of the bug: is it due to a difficulty writing a subtle algorithm, or is it due to a difficulty understanding the Go language's semantics.
If it's the latter, then TLA+ isn't the right tool, and neither is SPIN. There are other tools for verifying language semantics. If it's the former -- i.e. the author of the spec knows the meaning of each line and its intent -- then TLA+ is a very good tool, but then a simpler spec could suffice, perhaps something like this: https://pron.github.io/files/Channels.pdf
The point was to do demonstrate the bug while staying close to the Go example. You can find the bug at a higher level, but then there's the objection that you're not finding the bug in the Go code, you're finding the bug in simpler toy code. That raises the further objection that we only find the bug because we were looking for it, which is why I showed we find the bug even if we do a straightforward translation of the code.
I understand, but I think this strikes at the core of our pedagogical differences regarding TLA+ -- after all, TLA+ is super-Turing-complete, and even TLC can check a subset of TLA+ that is still effectively Turing-completish. Of course you can specify at any level in TLA+, and people have even written compilers from C and Java to TLA+. But doing so suffers from the same scalability problems that all code-level verification techniques suffer from.
The question we're asking is how best to get people to use TLA+. Do you show them what model-checking can do and then show that TLA+ can model virtually anything and TLC can check many things, and do so at the code-level because that is something they already know from programming -- but then they ask, as they do in this discussion, why you need TLA+ at all if all you're doing is translating Go to some other language -- or do you first try to show them the TLA+'s real strength, which is mathematical modelling of systems, but that is a new concept that is different from programming and can be foreign to them?
It's a hard problem, and maybe the right approach is to do both, which is what you're doing if we take this post together with others you've written. But I think it's worth mentioning that in this case, this is not the spec someone who knows both TLA+ and Go well would likely write.
BTW, I'm trying to remember which of those two features sold me on TLA+, and I think it was the combination of both. I knew the limitations of model-checkers (and had worked with NASA's Java model-checker before) that I knew that a model-checker alone wouldn't give me what I need for the complex distributed system I was working on, and mathematical modelling alone of something so subtle wouldn't have sufficed either without some help checking (cheaply!) if my ideas were right or wrong. So neither aspect would have sold me in isolation, I think.