I recently learned about TLA+ and are asking myself if Satoshi used this for the design of concurrent and distributed systems like BitCoin?

http://lamport.azurewebsites.net/tla/tla.html

http://lamport.azurewebsites.net/tla/hyperbook.html

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-spec-tla-plus.pdf