I work a lot with a proof assistant called Coq, and I have found it a very joyful experience.
- Visit Cocorico!, the Coq Wiki
- Here you can see some of the older stuff I have proved using Coq (This is my original formalisation of constructive real numbers in Coq).
- continued fractions: how to add and multiply them?. Beware of the code, it is not proven to be correct yet!
- Stern-Brocot Arithmetic, implemented in Haskell and verified in Coq.
- Coinductive field of exact real numbers, as a good example of general corecursion in Coq.
- A library for working with bisimulation, coalgebras, and λ-coiteration.
- Problem 11262 of The American Mathematical Monthly, formalised in Coq.
- Coq support for enscript
- Alternating bit protocol in Maude, using Kahn process networks.