AI-Assisted Formal Specification and Verification in Dafny: A Multi-Provider VS Code Extension

Abstract

Formal software verification represents an essential approach for ensuring correctness and reliability of critical systems, yet faces significant barriers due to the complexity of manually specifying method contracts, loop invariants, and other verification constructs. This dissertation addresses this limitation through the development of an advanced Visual Studio Code extension that automates the generation for formal specification and verification constructs using multiple artificial intelligence providers. The work extends the original implementation of a VSCode extension for Dafny, transforming an initial prototype into a robust and scalable platform for formal verification assistance. The solution implements a multi-provider architecture that integrates AI services including OpenAI, Claude, and DeepSeek through a unified interface, with intelligent fallback mechanisms ensuring continuous availability even during individual service disruptions. Firebase integration enables dynamic configuration management and secure credential storage, making it suitable for both academic and industrial environments. Experimental validation through a controlled crossover design study performing a total of 42 formal specification and verification tasks demonstrates the effectiveness of the proposed approach. Results reveal a System Usability Scale score of 74.6/100, indicating good user acceptance. Comparative analysis shows significantly superior success rates for AI-assisted approaches (85.7%) compared to manual methods (42.1%). Temporal efficiency evaluation demonstrates 43.8% productivity gains, with average completion times of 6.25 minutes for tool-assisted approaches versus 11.12 minutes for manual methods. The contributions of this research include the empirical validation of three established research questions: (1) How is the usability and level of user experience of the multi-provider AI verification assist plugin?; (2) How do the success rates of verification specification generation compare between manual and AI-aided approaches?; and (3) How does the time efficiency of verification specification generation compare between manual and AI-aided methods? This work further demonstrates the viability of multi-provider architectures for AI-assisted development tools, and establishes replicable experimental methodologies for evaluating formal verification tools. The results suggest that intelligent integration of multiple AI providers can significantly improve the accessibility and effectiveness of formal software verification. The enhanced platform establishes a foundation for more reliable, secure, and empirically validated AI-assisted formal verification tools, bridging the gap between research prototypes and production-ready development environments. Future work directions include expanded experimental validation with larger participant cohorts, integrated tutorial systems for educational applications, and advanced verification construct generation including automated lemma synthesis.