The scientific objectives of VeriDis are to combine methods, tools, and techniques for the verification of distributed algorithms and systems. In particular, the teams in Nancy and Saarbrücken are developing the VeriT SMT solver and the Spass theorem prover.
I am a member of the project Tools and Methodologies for Formal Specifications at the Joint Centre of INRIA and Microsoft Research in Saclay, close to Paris. This project funds much of the development of TLAPS, the TLA+ Proof System.
Some supplementary material on the design of TLAPS and its back-end provers is available here.
Our largest case study so far on the use of TLAPS, carried out as part of two PhD projects, concerns the formal verification of a variant of the Pastry algorithm, and is documented here.