[SystemSafety] Empirical Study on the Correctness of, Formally Verified Distributed Systems

[Derek M Jones]

All,

"This paper thoroughly analyzes three state-of-the-art, formally
verified implementations of distributed systems: Iron-
Fleet, Verdi, and Chapar. Through code review and testing,
we found a total of 16 bugs, many of which produce serious
consequences, including crashing servers, returning incorrect
results to clients, and invalidating verification guarantees.
These bugs were caused by violations of a wide-range
of assumptions on which the verified components relied."

https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com