# Spin A [[Formal Methods]] tool based on [[Model Checking]] that is often used to verify [[Multithreading]] applications. In [Finding Goroutine Bugs with TLA+ • Hillel Wayne](https://www.hillelwayne.com/post/tla-golang/) (see [[ZK - 2g3a - golang Concurrency is not easy]]), [[Hillel Wayne]] mentions that [[Spin]] has a channels primitive that can be used to model [[golang channels]], and has previously (the file got deleted) been used to model the runtime [[Scheduler]]: [runtime: delete proc.p · golang/go@0e027fc · GitHub](https://github.com/golang/go/commit/0e027fca428a893ceeb49e4f833f9a923c5f201d) (the code review mentions [[Dmitry Vyuokov]]). ## Links - [Spin - Formal Verification](http://spinroot.com/spin/whatispin.html) - [Concise Promela Reference](http://spinroot.com/spin/Man/Quick.html)