formal methods tool developers

Abstract: We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to the EP calculus for higher-order logic and integrate it into the automated theorem prover Leo-III. The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse. The implementation uncovered several bugs in Leo-III.

Abstract: The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-quality mechanization in Rocq. This mechanization uses a number of Rocq features in sophisticated ways, including a carefully constructed algebraic hierarchy for modeling separation logic resources, and a proof mode for embedded separation logic proofs, which combines custom Ltac with extensible typeclasses. The library has been developed for over a decade with dozens of contributors, with an emphasis on modularity and maintainability. We explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris. Using these features, we provide a novel implementation of the Iris proof mode with improved performance, simplify the handling of equivalences through quotient types, build a variant of Diaframe proof automation, and provide convenience features like automatic construction of Iris fixed points. Building on Lean lets us integrate with the extensive Mathlib library, allowing us to re-use results from this library for program verification tasks that have heavy mathematical dependencies, as we demonstrate with an application to probabilistic program verification.

Abstract: A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP benchmark. We experimentally study the impact of the approach across several ITP-derived benchmark sets and its interaction with theorem proving strategies. We find that while the neural guidance consistently improves performance within individual benchmark domains, cross-benchmark application of guiding models underperforms the plain default strategy. This can be remedied by training a single model on all datasets at once. Such a model, although more expensive to obtain, helps Vampire almost catch up in performance across all datasets. The picture when considering combined strategies is less clear-cut, indicating persisting value of neural guidance but under diminishing returns.