Tools for Proofs

Goals of the project

TLA+ is a specification and proof language based on temporal logic, where first-order logic and set theory are used to describe a set of states and the possible transitions between these states. TLA+ also includes a module system for manipulating large-scale specifications.

There are a number of existing tools for working on TLA+ specifications, the most important of which is the TLC model-checker. Although the proof side of TLA+ is not well-developed yet, with no proof tools and an incomplete definition of the proof language, TLA+ has already proved its worth in significant projects in hardware design (Alpha and Itanium processors), protocols (PCI-X), and software (Doligez-Leroy-Gonthier garbage collector).

In this project, we are working on turning TLA+ into a complete solution for writing, debugging, and proving specifications. More precisely, we are concentrating on the proof aspect:

  • refining the proof language
  • developing and adapting automatic tools to help users prove TLA+ theorems (Zenon, veriT)
  • providing an interface between the automatic provers and the TLA+ development environment
  • translating TLA+ proofs into a machine-checkable format for verification by an independent checker (Isabelle)

We will validate and enhance our tools by finding examples of real-world projects where formal specifications bring real improvements over other methodologies. Feedback from these examples will help us improve the proof language and the tools and develop methods and “design patterns” for using TLA+.