Field Testing Stainless by Verifying Daisy’s AST Library

Automation is rapidly transforming industries, shifting responsibility from human workers to machines. However, since machines lack sentience, ensuring correctness falls on developers. Formal methods offer a rigorous approach to provide strong correctness guarantees, but their adoption remains limited due to usability challenges such as steep learning curves and language limitations. We focus on a subset of formal methods: deductive verifiers. These mitigate usability challenges by automating large portions of the verification process. This work uses a deductive verifier for Scala: Stainless. We verify the abstract syntax tree (AST) package of a library used in practice: Daisy, a mature static analyser that optimises and verifies finite-precision code. Our methodology breaks down the verification process using informal package specifications. We then derive formal specifications for functions and algebraic datatypes from these informal guidelines and verify that the implementation adheres to the formal specifications. We increase the amount of verified code used in practice and contribute insights from the process to tool developers and users. In particular, some of the results we present are: (1) A verification of Daisy's optimisations over ASTs (e.g., that $0 + lhs \to lhs$ preserves semantics); (2) Limitations in Stainless that contribute to the code bloat of 3:1 between specifications and functionality; (3) Synergies between our modular methodology and Stainless's annotations.