Séminaire LSL - Loïc Correnson - Packaging proofs with Why3find

Abstract

With the increasing maturity of proof assistants, diving into the development of large theories is appealing, but existing toolchains might not scale. Although standard software engineering methods can be applied to mechanized proof development, specific issues shall be addressed. In this article, we focus on the Why3 platform. We present why3find, an independent tool for supporting the development of large, trustworthy Why3 packages. Why3find is designed to address common issues encountered in real world industrial developments based on formal methods. It proposes Why3-based solutions for configuring projects, managing dependencies, proving and checking proofs, tracking axioms and possible inconsistencies, extracting code, generating documentation and distributing packages.