TLA+ | The way to specify

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, protocols and software.

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
• making a development environment for TLA+ specifications and proofs
• developing and adapting automatic tools for helping to prove TLA+ theorems (Zenon, haRVey-SAT)
• 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+.

Team and former Members

• Leslie Lamport (Microsoft Research)
• Stephan Merz (LORIA)
• Damien Doligez (INRIA)
• Daniel Ricketts (INRIA)
• Denis Cousineau (MSR-INRIA)
• Kaustuv Chaudhuri (MSR-INRIA)
• Simon Zambrovski (Microsoft Research)

Status

Project is in progress…

Project Homepage

http://www.msr-inria.inria.fr/Projects/tools-for-formal-specs/