Currently, Verdi's file operation semantics assumes a stable and atomic storage, which is unrealistic and has led to bugs like uwplse/verdi-raft#51. One option to address this is to connect the semantics to a verified crash-safe file system such as FSCQ.