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:

- CompCert
- Vellvm
- Bedrock
- Ynot
- RockSalt
- Frenetic
- seL4 (not in Coq)
- Four Color Theorem
- Homotopy Type Theory
- Flocq

Some classic papers on automated theorem proving and verification: