主要观点：CertiCoq 是 Coq 证明助手规范语言 Gallina 的编译器，目标是 Clight 语言，部分编译器已验证，部分正在验证。提供了相关文档、安装说明、成员信息、许可证及目录结构等。
关键信息：

• 可通过CertiCoqWiki获取使用 CertiCoq 插件及相关演示的信息。
• 安装说明见INSTALL.md。
• 现任成员有 Andrew Appel 等，过往成员有 Abhishek Anand 等。
• 遵循 MIT 许可证。
• 目录结构包含theories/等多个子目录及各子目录下的具体内容。
• 使用 github 的issue tracker跟踪 bugs 和功能请求。
  重要细节：
• CertiCoq 编译器的不同部分验证状态不同。
• 文档中有关于编译 Gallina 到 C 及与生成的 C 代码交互的指导。
• 目录结构中各子目录的具体功能和包含的源代码。