Thursday 27 April 2023, 14:00, room 1Z28: Reconstruction of TLAPS proofs solved by veriT in Lambdapi, Alessio Coltellacci (Université de Lorraine, Inria Nancy).

TLAPS provides an interactive environment for proving properties of TLA+ specifications. It integrates automatic proof search backends to discharge proof obligations, such as satisfiability modulo theories (SMT). Nevertheless, to maintain the trustworthiness of proof generated by an SMT-solver, we intend to reconstruct the resulting SMT proofs into Lambdapi. We will present our progress on the development of an automatic tool that aims to reconstruct veriT proof trace of TLAPS proof obligation in Lambdapi, and the TLA+ semantics defined in Lambdapi.