Validating Safety Arguments with Lean

Abstract

Safety Assurance Cases (ACs) are structured arguments which demonstrate that a system fulfills its safety requirements. However, the reasoning used in ACs is often presented informally and thus difficult to rigorously evaluate. To protect against the acceptance of ACs based on fallacious reasoning, our previous work has proposed a framework for formalizing fragments of ACs and verifying their reasoning using the Lean Theorem Prover. This work expands on the use of Lean to automatically validate fragments of ACs, identifies challenges faced by AC developers who wish the leverage theorem proving software, and demonstrates our approach to mitigating these challenges.