I am a huge fan of mm0, the thesis[0] is so brilliantly written, and MMC is such a great step towards the kind of verified computing I really want to be doing

[0]: https://digama0.github.io/mm0/thesis.pdf