I wonder if it's possible to model how fucked up the Golang concurrency model is with TLA+?

As a TLA non-SME I couldn't say, but would definitely find it useful and probably impressive. Maybe Brad Fitzpatrick could team up with Aphyr and use it to make golang v2 a bit less crap.

Note: I write this with love, as someone who's written hundreds of thousands of lines of Go, and am now turned off and afraid of the behavior at the sketchy edge boundaries. I've now shifted to learning Rust, albeit slowly and finding it saddeningly challenging compared to what I can pump out with the Go.

For reference, see "Data Race Patterns in Go", posted 21 days ago: https://news.ycombinator.com/item?id=31698503