Technical Summary: Toward Practical Deductive Verification

Problem Statement

Despite the proven feasibility and effectiveness of deductive verification in high-profile projects (e.g., seL4, Ironclad, CakeML), the technique remains a niche practice rather than a mainstream engineering standard. While theoretical foundations and tools have advanced, there is a lack of empirical understanding regarding the practical conditions that enable successful applications and the specific barriers preventing broader adoption in industry and academia. Existing literature often focuses on individual case studies or theoretical techniques, leaving a gap in knowledge concerning the holistic workflow, maintenance issues, and human factors involved in real-world deductive verification.

Methodology

The authors conducted a qualitative study adhering to the ACM SIGSOFT Empirical Standard for qualitative surveys.

• Data Collection: The study involved semi-structured interviews with 30 practitioners from 17 institutions across Europe, America, and Asia. The participant pool included doctoral students, senior researchers, and software developers/proof engineers, with a significant focus on industrial contexts (27 of 30 interviews discussed industrial projects).
• Participants: The cohort had diverse experience levels (ranging from <1 to >10 years) and utilized a wide array of tools, including automated deductive verifiers (Dafny, F*, Verus, Viper, Why3) and interactive theorem provers (Rocq, Isabelle, Lean).
• Analysis: The researchers employed the thematic analysis approach by Braun and Clarke. This involved familiarization with data, open coding, and the iterative development of themes. The analysis was conducted by two interviewers to ensure coherence and minimize bias, resulting in a finalized codebook and five overarching themes.

Key Contributions

The paper makes four primary contributions:

1. Empirical Understanding: A detailed account of practitioner opinions and experiences regarding the practical application of deductive verification.
2. Extraction of Factors: The identification of four success factors and five main barriers that provide a principled account of when and how verification yields value.
3. Highlighting Underexplored Issues: The surfacing of critical, often neglected challenges, specifically proof maintenance during code evolution and the complexities of verification debugging.
4. Actionable Recommendations: Concrete guidelines for practitioners, tool builders, and researchers covering usability, automation strategies, and workflow integration.

Key Results and Findings

1. Verification Applicability and Cost-Benefit

Success is heavily dependent on the criticality of the software and the clarity of requirements. Practitioners find verification most viable for critical components (e.g., security, concurrency) where the cost-benefit ratio is favorable. A major barrier is the perception that verification is "ridiculously expensive" and often fails to pass cost-benefit analysis for general-purpose code. Well-defined requirements are a prerequisite; ambiguous requirements make specification formulation intractable.

2. Managing Technical Complexity

• Fundamental Challenges: Quantifiers, induction, recursion, and loop invariants remain difficult.
• Proof Strategy: Structuring proofs is a significant hurdle. While compositional reasoning and modularity are valued for scalability, practitioners often find the manual effort required to split proofs and define sub-analyses burdensome.
• Abstraction and Simplification: Users frequently resort to abstraction or simplifying the code/model to make verification tractable, though finding the right level of abstraction is itself a complex task.
• Specification Engineering: Writing specifications is often the bottleneck, not the proof itself. Translating user intent into formal specifications is difficult, and determining the "right" strength of a specification (useful yet provable) is a major challenge.

3. Tool Maturity and Automation

• Automation Paradox: Automation is viewed as both a "blessing and a curse." While it reduces manual proof effort, it often lacks fine-grained control. Users struggle with "black box" behaviors where SMT solvers fail without clear feedback, or where the tool requires manual context reduction to avoid saturation.
• Performance: Performance is a critical concern, particularly for SMT-based tools. Nonlinear arithmetic and large proof contexts frequently cause timeouts or unacceptable delays (e.g., >30 seconds).
• User Experience: Tools often lack maturity in terms of IDE integration, debugging support, and documentation. Users desire features like counterexample generation, axiom profiling, and visibility into intermediate proof states to distinguish between tool failures and actual bugs.

4. Integration and Maintenance

• Workflow Integration: Verification must align with existing development practices (languages, CI/CD). Forcing engineers to adopt entirely new workflows or languages is a significant adoption barrier.
• Proof Maintenance: This emerged as a major, underexplored obstacle. As code evolves, proofs often break ("random proofs breaking CI"), and there are no mature solutions for automated proof repair. This leads to a preference for verifying "frozen" code rather than evolving systems.
• Readability: Automatically generated code or code interleaved with annotations often suffers from poor readability, causing pushback from engineering teams.

5. Expertise and Mindset

Verification requires a distinct mindset and specialized expertise that differs significantly from standard software engineering. The steep learning curve and the cognitive shift required to think formally about correctness are major adoption barriers. Knowledge transfer is difficult due to the lack of standardized documentation for proofs and techniques.

Significance and Recommendations

The paper claims significance as the first qualitative investigation grounded in data across the entire deductive verification community, moving beyond individual case studies to identify systemic issues.

For Practitioners:

• Focus verification efforts on critical system components rather than attempting full-system verification.
• Integrate verification early in the development lifecycle but balance this with the need for code stability to mitigate maintenance costs.
• Invest in training to bridge the expertise gap.

For Tool Builders and Researchers:

• Usability: Develop tools with better IDE integration, debugging support (e.g., counterexamples, intermediate state inspection), and documentation.
• Automation Balance: Create systems that balance high automation with user control, allowing engineers to guide the verification process and understand tool internals.
• Maintenance: Investigate techniques for proof repair and managing the interaction between verified and unverified code.
• Education: Revise pedagogy to include practical application of state-of-the-art tools and systematic catalogs of "idiomatic" proofs, moving beyond theoretical exercises.

The authors conclude that while deductive verification is powerful, its widespread adoption depends on addressing the "human" and "process" factors—specifically maintenance, usability, and the integration of verification into the natural flow of software development—rather than solely focusing on theoretical advancements.