# Rocq-Grok 技能详解 Rocq-Grok 是一款面向 Rocq（原名 Coq）证明开发的智能代理技能包，为代理提供理解、构建、修复和审查证明的工作流程。适用于处理 `.v` 文件、`_CoqProject` 配置、定理陈述、证明目标、依赖类型、证明策略（tactic）失败、构建失败、以 `Admitted` 暂时跳过的证明义务、假设审计和反例等场景，也支持软件不变量、合约及新项...