CertiuCOS2

Using Coq
1

Has anyone studied the CertiuCOS2 project? The code looks abstract without comments, and I’m looking for someone to study it with.