https://dafny.org/blog/2023/04/19/making-verification-compelling-visual-verification-feedback-for-dafny

https://dafny.org/blog/2023/07/14/types-and-programming-languages/

https://dafny.org/blog/2023/08/14/clear-specification-and-implementation/

https://dafny.org/blog/2023/10/27/proof-dependencies/

https://dafny.org/blog/2023/11/08/cracking-the-coding-interview-in-dafny-permutations/

https://dafny.org/blog/2023/12/01/avoiding-verification-brittleness/

https://dafny.org/blog/2023/12/06/automated-test-generation-chess-puzzles-with-dafny/

https://dafny.org/blog/2023/12/20/standard-libraries/

https://dafny.org/blog/2024/01/12/semantics-of-regular-expressions/

https://dafny.org/blog/2025/06/24/evm-bytecode/

https://dafny.org/blog/standard-libraries/2025/12/01/statistics-library/

https://medium.com/data-science/nine-rules-to-formally-validate-rust-algorithms-with-dafny-part-1-5cb8c8a0bb92
https://towardsdatascience.com/nine-rules-to-formally-validate-rust-algorithms-with-dafny-part-2-f2a279686700/

ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
https://arxiv.org/pdf/2512.10173

A benchmark for vericoding: formally verified program synthesis
https://arxiv.org/abs/2509.22908

Formal Verification of Minimax Algorithms
https://arxiv.org/abs/2509.20138

MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
https://arxiv.org/abs/2512.10187

Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
https://arxiv.org/abs/2507.03659