Details

Formal Verification of Safety-Critical Numeric and Validation Algorithms Using Dafny and SMT Solvers

Year: 2026

Term: Winter

Student Name: Ajaan Nalliah

Supervisor: Doug Howe

Abstract: Safety-critical software systems require correctness that the standard testing practices do not provide. This project dives into the practical applications of Dafny, which is an SMT-based automated verification language, for formally specifying and verifying safety-critical numeric, validation, sorting, and graph algorithms. Six algorithms were implemented and verified: Luhn checksum validation, ISBN-10 and ISBN-13 verification, safe arithmetic operations with overflow protection, selection sort, Dijkstra’s shortest path algorithm, and the Sieve of Eratosthenes, which resulted in 909 lines of verified Dafny code which is supported by Z3 SMT solver. The project addresses three research questions regarding the expressive nature of Dafny along with its practicality, the specification patterns that determines the SMT solver performance, and the boundaries of automated verification for common algorithmic constructs. Empirical measurements across all of the six algorithms resulted in an aggregate proof-to-code ratio of 0.77x and a total verification time of 11.5 seconds, which is a substantially less overhead than comparable prior work in interactive theorem provers such as Isabelle/HOL and Coq. Four of the six algorithms required zero manual proof construction, where the remaining overhead concentrated in Luhn’s traversal equivalence lemmas and Dijkstra’s path witness infrastructure. Six specification patterns were identified that consistently appears when supporting automated verification: the structural alignment between specification and implementation, witness-based correctness with respect to existential properties, lemma hierarchies based on inductive reasoning, ghost predicate packaging, encapsulating mutations within verified helper methods, and explicit calculational proof steps. However, automated verification struggled with universal quantification across unbounded domains, structural induction over recursive data structures, and connecting abstract specification predicates to concrete program state, such that the limitations that required specification redesign instead of solver tuning each individual case.