openmath-rocq-theorem
AdvisoryAudited by Static analysis on Apr 30, 2026.
Overview
No suspicious patterns detected.
Findings (0)
Artifact-based informational review of SKILL.md, metadata, install specs, static scan signals, and capability signals. ClawScan does not execute the skill or run runtime probes.
The agent may run local tooling in the theorem workspace, which can read proof files and affect build outputs.
The skill clearly discloses local command execution. This is expected for Rocq proof setup and verification, but users should be aware that the agent may run build and environment-check commands locally.
side_effects: - Runs local Rocq, dune, and opam commands in the theorem workspace
Use the skill only in the intended theorem workspace, review commands before running them, and keep work under version control.
Project dependencies may be installed persistently into the user's local Rocq/opam environment.
The opam dependency install step is purpose-aligned, but it relies on the downloaded project's opam file and may fetch or build packages into the active opam switch.
If the project has an `opam` file, install missing dependencies before proving: ```bash opam install . --deps-only ```
Review the project opam file first and prefer a dedicated opam switch for OpenMath theorem work.