Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work

Table of Links

• Abstract and Introduction
• Dancing Links
• The Rust Programming Language
• RAC: Hardware/Software Co-Assurance at Scale
• Rust and RAR
• Dancing Links in Rust
• Related Work
• Conclusion, Acknowledgments, and References

7 Related Work

A number of domain-specific languages targeting both hardware and software realization, and providing support for formal verification, have been created. Cryptol [5], for example, has been employed as a “golden spec” for the evaluation of cryptographic implementations, in which automated tools perform equivalence checking between the Cryptol spec for a given algorithm, and the VHDL implementation.

Formal verification systems for Rust include Creusot [8], based on WhyML; Prusti [3], based on the Viper verification toolchain; and RustHorn [20], based on constrained Horn clauses. AWS is developing a model-checker for Rust, Kani [2]. Additionally, Carnegie-Mellon University is developing Verus, an SMT-based tool for formally verifying Rust programs [19]. With Verus, programmers express proofs and specifications using Rust syntax, allowing proofs to take advantage of Rust’s linear types and borrow checking. It will be interesting to attempt the sorts of correctness proofs achievable on our system using these verification tools