Research engineer (post-doc) at MSR-Inria Joint Centre

by Stephan Merz, March 5, 2018

The Microsoft Research-INRIA Joint Centre is offering a 24-month position for a
research engineer to contribute to the design and further development of the
TLA+ Proof System.

TLA+ ( is a language for specifying and reasoning about systems, including concurrent and distributed systems. It is based on first-order logic, set theory, and temporal logic. TLA+ and its tools have been used in industry for more than a decade. More recently, we have extended TLA+ by a language for writing structured formal proofs and have developed TLAPS (, a proof checker that contains an interpreter for the proof language and interfaces with different back-end provers, including SMT solvers, the tableau prover Zenon that supports set-theoretic constructions, and a declarative encoding of TLA+ set theory as an object logic in the logical framework Isabelle. TLAPS is integrated into the TLA+ Toolbox, an IDE for TLA+.

Although it is still under active development, TLAPS is already quite powerful and has been used for several verification projects, in particular in the realm of distributed algorithms (e.g.,

The current version of TLAPS handles the "action" part of TLA+: first-order formulas with primed and unprimed variables that represent the values of a variable before and after a transition. It also supports the propositional fragment of temporal logic. This fragment is enough for proving safety properties (invariants and step simulation). We have initiated a complete rewrite of the code base, with the aim of providing support for module instantiation and for the full temporal logic of TLA+, which will allow us to prove liveness and refinement properties.

Description of the activity of the research engineer

The research engineer (post-doctoral) position is funded for 24 months by the Microsoft Research - Inria Joint Centre. You will work together with the members of the TLA+ project, including Damien Doligez, Leslie Lamport, and Stephan Merz on extending the TLA+ Proof System. Your main objective will be to complete the rewrite of the existing version of TLAPS so that it can be released to users of the prover. You will also be able to work on extensions of existing functionality, including the following items:

  • Module instantiation. The TLA+ language contains a module system, and modules can have constant and variable parameters in order to make them generic and reusable. When a module is instantiated, parameters can be replaced by constant- and state-level expressions, and these instantiations must be taken into account when generating proof obligations for back-end provers.
  • Handling temporal logic. Proofs of liveness properties need support for reasoning about first-order temporal logic, such as induction over well-founded orderings. Fairness hypotheses require reasoning over the enabledness of actions. New backend provers need to be set up and integrated into TLAPS for carrying out these proofs.
  • Improved backend provers. The current backend provers provide decent support for proof obligations mixing first-order logic, elementary set theory, functions, and integer arithmetic. Reasoning about other important data structures such as finite sequences requires low-level user interaction. We are interested in exploiting advances in automatic deduction techniques, such as support for relevant theories in SMT solvers, for enabling a higher degree of automation of such proof steps.
  • Rigorous validation of soundness. Computing proof obligations involves some subtle transformations, such as distributing the prime operator of TLA+ or handling instantiated ENABLED expressions. We are working on a precise definition of the semantics of the proof language that would help us ensure the soundness of these transformations and give guidelines to the implementation.
  • Checking SMT proofs. The SMT backend handles most of the proof obligations that occur in practice. The current version of TLAPS assumes the external SMT solver to be correct, but we are interested in reconstructing proofs provided by SMT solvers within Isabelle/TLA+. The Zenon backend already benefits from proof reconstruction.
  • Performance issues. Proof projects can be large, and TLAPS implements mechanisms, such as fingerprinting proof obligations, that are intended to make the tool scale. Performance bottlenecks should be monitored and avoided, whenever possible.
  • Case studies and proof libraries. Our work on TLAPS is validated by carrying out case studies, and we provide libraries of lemmas that are useful for many proof projects.

We do not expect to be able to address all of these issues within 24 months. The choice of items will be made jointly with the research engineer, also depending on his or her interests and background.

Skills and profile of the candidate

You should hold a PhD degree in computer science and have solid knowledge of mathematical logic, as well as implementation skills related to symbolic theorem proving. TLAPS is mainly implemented in OCaml, but some Java programming will be necessary for interfacing TLAPS with the other TLA+ tools. Experience with temporal and modal logics, with interactive theorem provers or with Eclipse could be valuable.

Work on TLAPS provides the opportunity to learn about issues of using deductive verification in practice, and there are possibilities to produce publishable research. However, the main focus is on the implementation of components of our tool chain that are missing or need improvement. 

Given the geographical distribution of the members of the team, we highly value a good balance between the ability to work in a team and the capacity to propose initiatives.



The research engineer can choose between working at the Microsoft Research - Inria Joint Centre in Paris or at the LORIA laboratory in Nancy.


The salary will be between 2900 and 3800 euros, depending on qualifications and experience.


The post is for a duration of 2 years, extensible to a 3rd year (depending on funding).


Candidates should send a resume and the names and e-mail addresses of two references to Damien Doligez <>, preferably by March 12, 2018. Please at least let us know if you are interested in the position or if you have any questions.

We intend to hire the research engineer by June, although the exact date is negotiable.