In terms of academic skills, these opportunities will immerge the candidate in the realm of interactive theorem proving and offer her/him the opportunity to acquire or improve a first experience with Coq. In terms of professional skills, it will allow her/him to acquire a first experience with the emerging profession of ``proof engineer'' as witnessed by many job offers such as the one found here .