Distributed で Concurrent なシステムの正しさを証明するための仕組み・言語 TLA+ https://lamport.azurewebsites.net/tla/tla.html

なんかすごそう