Thomas L. Rodeheffer
12 February 2013
This report presents a formal specification, written in TLA+, for the Naiad Clock protocol, along with the results of checking the specification using the TLC model checker. Also presented is a formal proof of the Naiad Clock safety properties, which has been mechanically checked using the TLA+ proof system.
This report is based partly on work with Martin Abadi, Frank McSherry, and Derek Murray.
Publisher Microsoft Technical Report
Copyright (c) 2013 Microsoft Corporation.