This paper describes the formal verification of two Turing machines using the program verifier Dafny. Both machines are deciders, so we prove total correctness. They are typical first examples of Turing machines used in any course of Theoretical Computer Science; in fact, the second machine is literally taken from a relevant textbook. Usually, the correctness of such machines is made plausible by some informal explanations of their basic ideas, augmented with a few sample executions, but neither by rigorous mathematical nor mechanized formal proof. No wonder: The invariants (and variants) required for such proofs are big artifacts, peppered with overpowering technical details. Finding and checking these artifacts without mechanical support is practically impossible, and such support is only available since recent times. But nowadays, just because of these technicalities, with such subjects under proof a program verifier can really show off and demonstrate its capabilities.

翻译：本文描述了使用程序验证器Dafny对两台图灵机进行形式化验证的过程。两台机器均为判定器，因此我们证明了其完全正确性。它们是理论计算机科学课程中典型的图灵机入门示例；事实上，第二台机器直接取自相关教科书。通常，此类机器的正确性仅通过对其基本思想的非形式化说明辅以少量示例运行来论证，既缺乏严格的数学证明也缺少机械化的形式化验证。这不足为奇：此类证明所需的（归纳）不变量（与变式）是包含大量技术细节的复杂构造体。在没有机械辅助的情况下发现并验证这些构造体实际上是不可能的，而此类辅助工具直到近年才得以实现。但如今，恰恰由于这些技术复杂性，以此类对象作为验证目标时，程序验证器得以充分展现其能力。