Interesting Coq Projects

This is a collection of Coq projects I find particularly interesting for one reason or another.

Projects

Name	Categories	Notes
Software Foundations	Theory of Computation, High-Assurance Computing	In my opinion, the greatest resource for learning Coq (or the foundations of verification in general). Completely free, incredibly easy to read, no confusing notation, and the textbook source is Coq files that you can download and work in.
Source-free, Machine-checked Validation of Native Code in Coq	High-Assurance Computing	A platform for verifying the correctness of binary code. The below-mentioned `memset` proof was written in (a much more recent version of) this system.
MetaCoq	Theory of Computation	“MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.”
A Formalization of Elements of Special Relativity in Coq	Physics	So far, the only paper I've seen exploring axiomatic physics in Coq. The code is painfully undocumented and I have not been able to find the author on any other platforms.

Name	Categories	Notes
Software Foundations	Theory of Computation, High-Assurance Computing	My solutions are not public due to an explicit request by the authors not to publish solutions. The linked repository is the list of exercises I've completed.
VOLPIC	High-Assurance Computing	A verification pipeline for Pascal source code.
`memset`	High-Assurance Computing	Verified the correctness of the `memset` function on Arm32 platforms. The proof is not yet public.
Haskell Curry's Living Thesis	Theory of Computation	An in-progress Coq implementation of Haskell Curry's Ph.D. thesis. This project is between refactors at the moment, I'm having a hard time deciding how close I want the proofs to be to their originals. Curry does not use constructivist logic for his proofs here, causing the trouble.
Coq Physics Experiments	Physics	A collection of attempts at formalizing some mathematics required for physical systems. A large portion of it was initially written as I followed along with Terence Tao's “Analysis I”. This is generally un-maintained.