Automata Learning algorithms such as Angluin’s L* have been widely used in the testing and specification inference communities. Yet, the correctness of these algorithms has not yet been formally established by mechanised proof.
As these algorithms are somewhat involved but relatively easy to specify, they are a perfect project to gain experience with interactive theorem proving and to evaluate ITP tools for their suitability for program verification.
Experience with these algorithms is not required, but experience with a proof assistant (such as Isabelle/HOL, Agda, or Lean) is required.