A very interesting paper and approach (but a bit hard to read at the pace of HN in order to post a timely comment :-).<p>I like the idea to focus first on the ideal case with no node failure nor network glitch, and to use then system transformers to introduce, in a formally verified way,
both the mechanisms and the failures to cope with.<p>I have now to find time to give it a try !<p>By the way, a bit of DuckDuckGo gives:<p>- <a href="http://verdi.uwplse.org/" rel="nofollow">http://verdi.uwplse.org/</a><p>- <a href="https://github.com/uwplse/verdi/" rel="nofollow">https://github.com/uwplse/verdi/</a>