September 2022:

  • Database gathering proofs from the proof systems Coq, HOL-Light and Matita, and their translations.

March 2023:

  • Inventory of automated theorem provers producing proofs, description of proof formats, and inventory of checking tools for these proof formats.

  • Comparison of the approaches used in the international Software Verification competition SV-COMP.

  • Definition of a mathematical framework for modular reasoning about type theories and their extensions.

September 2023:

  • Release of software for translating proofs coming from important proof systems based on type theory like Isabelle, Agda, PVS, Lean or Minlog, to Dedukti and back.

  • Software prototype for the automated inference of program specifications as logical axioms.

  • Tools for managing the dependencies between proofs, and querying and searching the database.

March 2024:

  • Detailed technical report on the evaluation of techniques for learning proof search guidance and premise selection in automated theorem provers.

January 2025:

  • Software for translating proof formats used by automated theorem provers to Dedukti.

September 2025:

  • Release of software for translating proofs coming from important proof systems based on set theory like Mizar, Atelier B or TLAPS to Dedukti and back.

  • Collection of verification challenges with summary of working recipes for verifying them.

  • Technique for syntax-semantics interface for program verification with or without type systems.

  • Extension of the database and associated tools to other systems like Agda, Minlog, PVS, Lean, Mizar, Atelier B, TLAPS.

  • White paper on including restricted natural language proof formats to existing proof libraries.

  • Prototype implementation of the mathematical framework, with basic user interface, user documentation and gallery of examples of type theories.