dafny-nfsd 使用顺序证明来验证崩溃安全的并发文件系统。目标是将goose-nfsd的经过验证的日记与Dafny中的顺序验证联系起来:想法是该日记应该使顺序推理成为顺序,在这种情况下,我们可以在像Dafny这样的生产证明系统中仅使用顺序推理来证明文件系统正确,同时携带排除了Perennial中复杂的并发性和崩溃安全性推理。 状态 编译中 运行make verify验证所有内容,并make compile以将文件系统和bank示例编译为Go(生成的代码进入dafnygen/ )。 您需要Dafny 3: 在Arch Linux上,您可以从AUR获取dafny-bin 在macOS上使用brew install dafny 对于其他系统,最简单的解决方案是从下载一个二进制发行版,将其解压缩,然后将其添加到您的$ PATH中(这是我们在CI中要做的,在Ubuntu 20.04上运行)。