Dafny was used to prove the correctness of the Lean implementation which was used to show the correctness of the Rust implementation.

The Dafny implementation served as an executable specification and could be used as a test oracle for coverage-guided testing of the Rust implementation.

The problem with heavily automated tools, like Dafny, is "proof brittleness": small changes in the code or theorem prover changes which proofs are accepted.

With Dafny, they could fairly easily prove the simple properties about the evaluator, such as "deny overrides allow".