Distributed protocols have been considered as one of too complicated structures to verify because of their intrinsic interleavings that may introduce state explosions. Serializability has been known as a crucial key to verify such protocols by ensuring that each trace of the target system is observably equivalent to a sequential trace. However, it is quite difficult to find good serializability conditions and it is even more difficult to prove the correctness. In this talk, we will show that there exist good serializability conditions and that the correctness can be proven automatically in a proof assistant.