Ideally, your project should relate to your current research and really spark your curiosity, nothing else will keep you cranking to that final Qed. It may be sufficient just to formalize a domain you want to work in, e.g. the ISA of a new architecture or network design. Projects that explore proof engineering challenges or help improve our tools would also be interesting. For example, check out the proceedings from User Interfaces for Theorem Provers (h/t Colin for pointing out this workshop!).
Some strategies for cooking up a project proposal:
Formalize a proof about your work or a seminal result in your area.
Extend an existing formally verified with some new feature.
Build automation for hairy proofs within an existing formally verified system.
More concrete examples:
Verify a simple bignum library in Bedrock and compare with this.
Building on Flocq or this, formalize error of floating point computations vs. reals and show a bound for an simple algorithm.
Explore improving the performance of the Coq proof checker.
Some successful projects you may want to extend or be inspired by:
Some classic papers on automated theorem proving and verification: