The burden of proof: automated tooling for rapid iteration on large mechanised proofs
File(s)
Accepted version
Author(s)
Tan, Chengsong
Donaldson, Alastair
Huerta y Munive, Jonathan Julián
Wickerson, John
Type
Conference Paper
Abstract
We report on challenges and solutions in making large mechanised proofs scale, based on our experience proving correctness properties for a cache coherence protocol. This was a difficult proof that required dozens of iterations to get right, and ultimately led to an inductive invariant with nearly 800 conjuncts, and to over 54,000 proof obligations. To address these proof engineering challenges we developed super_sketch, a tool that automates the generation of proofs involving multiple subgoals in Isabelle/HOL, enabling efficient management and maintenance of large-scale proofs. We further contribute super_fix, a tool to fix corner cases that cannot be fully automated with super_sketch, such as correcting proof scripts invalidated by upstream changes to definitions. This allowed us to drop simplifying restrictions in our model while retaining the correctness proof, as we avoid the significant manual effort that would otherwise be required to inspect and fix the broken lines of the original proof when generalising the model. Our work provides insights into proof engineering practices and highlights the need for improved support in proof assistants for large-scale mechanized proofs.
Date Issued
2025-06-12
Date Acceptance
2025-01-13
Citation
2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), 2025
ISSN
2575-5099
Publisher
IEEE
Journal / Book Title
2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE)
Copyright Statement
Copyright © 2025 IEEE. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Source
FormaliSE 2025 - International Conference on Formal Methods in Software Engineering (with ISCE 2025)
Place of Publication
Ottawa, ON, Canada
Publication Status
Published
Start Date
2025-04-27
Finish Date
2025-04-28
Coverage Spatial
Ottawa, Ontario, Canada
Date Publish Online
2025-06-12