openmath-rocq-theorem
AdvisoryAudited by VirusTotal on Mar 25, 2026.
Overview
Type: OpenClaw Skill Name: openmath-rocq-theorems Version: 1.0.3 The skill bundle provides a legitimate workflow for formal verification using the Rocq (Coq) proof assistant. It includes standard environment checks, build commands (dune), and dependency management (opam) appropriate for the stated purpose. No indicators of data exfiltration, malicious execution, or prompt injection were found in SKILL.md or the reference files.
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.