Fencing off Go: Liveness and safety for channel-based programming (blog.acolyer.org)

Very nice! How would you use it? Does the user make some kind of liveness assertion about a Go program which then gets model checked?

Channels were supposed to be a way to be better at preventing deadlocks than mutexes, in itself ( at the cost of some performance). What i found is that it makes the problem different but not much easier as soon as the problem grows. Using buffered channels, for example, may ends in having your program deadlock in an unreproductible way depending on the load and goroutine scheduling ( as soon as somewhere in your program there is a ring of goroutines communicating through buffered channels).

Just like with many things in go, it feels like a very raw basis for a good but yet to come langage.