Mechanical verification of concurrent systems with TLA

Abstract

We describe an initial version of a system for mechanically checking the correctness proof of a concurrent system. Input to the system consists of the correctness properties, expressed in TLA (the temporal logic of actions), and their proofs, written in a humanly readable, hierarchically structured form. The system uses a mechanical verifier to check each step of the proof, translating the step’s assertion into a theorem in the verifier’s logic and its proof into instructions for the verifier. Checking is now done by LP (the Larch Prover), using two different translations—one for action reasoning and one for temporal reasoning. The use of additional mechanical verifiers is planned. Our immediate goal is a practical system for mechanically checking proofs of behavioral properties of a concurrent system; we assume ordinary properties of the data structures used by the system.