Hacker News Reader

We are still vetting and improving the consensus algorithm, but we're planning on publishing a full TLA+ spec once the algorithm stabilizes.

Wouldn't it be easier to start with TLA+ / PlusCal? It offers higher level of abstraction and helps catch specification bugs.