As the demand for robust cybersecurity solutions grows, ensuring software is free from exploitable defects has become critical. Verification tools—programming languages or software designed to prevent such vulnerabilities—are becoming increasingly sophisticated, with artificial intelligence enhancing their accessibility and usability.

In a collaboration between Lancaster University and the Australian National University, a guide to one such verification tool, the Dafny programming language, has been developed. Dr Charles Weir, Senior Lecturer in Security and Protection Science at Lancaster University’s School of Computing and Communications, co-authored the paper with James Noble, Honorary Professor at the Australian National University. Their work explores how Dafny can empower developers to produce error-free code for secure and reliable digital systems.

Dafny stands apart from conventional programming languages by enabling programmers to define not only how their programs should function but also what they are intended to achieve. By leveraging artificial intelligence, Dafny compares these high-level specifications (the "what") with their actual implementation (the "how"), ensuring alignment and reducing errors. It compiles to C#, Java, or Python, so can be used very widely.

Despite its benefits, Dafny is widely regarded as a challenging language to master. Recognising this, Dr Weir and Professor Noble authored The Faultless Way of Programming: Principles, Patterns, Practices, and Peculiarities for Verification in Dafny. This beginner-friendly guide is tailored for experienced programmers who may not yet be familiar with software verification technologies. By following the paper, developers can efficiently learn to create functional and cyber-secure code across diverse applications.

The guide provides a step-by-step approach to learning Dafny, covering foundational concepts such as writing verifiable code, describing functionality within Dafny, and addressing common challenges encountered during programming. Published in the EuroPLoP 2024 Proceedings, the paper is now accessible online for developers seeking to deepen their expertise in verification technologies.

Dr Weir commented on the significance of the publication: “This paper was an exploration of a different way to support developer-centred security. Rather than relying solely on functional and penetration testing, why not use a language that inherently makes errors difficult to introduce? However, Dafny is notoriously difficult to learn, so we designed this paper to guide newcomers. As someone new to formal methods myself, I approached Dafny with a beginner’s perspective, which informed the structure of our guide. Writing this paper was a rewarding experience, and we hope it serves as a valuable resource for future developers.”

By simplifying the learning curve for Dafny, this work underscores Lancaster University’s commitment to advancing cybersecurity and empowering developers with tools that ensure safer, faultless programming.