etcd is based on Raft. Raft has a TLA+ spec. But do note that the implementation usually diverges from its algorithm [0].
For etcd, we try to keep the core algorithm as self-contained and deterministic (no I/O, no timer) as possible. So it can be very close to the pure algorithm. We are very confident about it since we throughly tested it, and the implementation is shared with other consistent large scale database systems too (cockroachdb, tikv).
ZooKeeper uses ZAB [1] under the hood. I do not think there is a TLA+ for ZAB.
For etcd, we try to keep the core algorithm as self-contained and deterministic (no I/O, no timer) as possible. So it can be very close to the pure algorithm. We are very confident about it since we throughly tested it, and the implementation is shared with other consistent large scale database systems too (cockroachdb, tikv).
ZooKeeper uses ZAB [1] under the hood. I do not think there is a TLA+ for ZAB.
[0] https://www.cs.utexas.edu/users/lorenzo/corsi/cs380d/papers/...
[1] http://www-users.cselabs.umn.edu/classes/Spring-2016/csci821...