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

there will be no proof ever in the future!

if true why should he proof it? which advantages will be the result? not a single advantage just many disadvantages.

LL is not in the position of CSW with Australian Taxation Office hunting him.

and he is the inventor of many other things he don't need the BitCoin inventor fame on top of the other things.

what maybe is possible that after his life time the truth about the inventor of BitCoin will be come to the light. maybe he will prepare something that should be revealed after he is not alive anymore.

watch nakamotofamilyfoundation.org. it could be the key to it.

---

Paxos Agreement - Computerphile

EDIT: http://nakamotofamilyfoundation.org/ is broken. where will the book have been published?