openmath-rocq-theorem

• Outcome: Review
• Latest audit: Sep 15, 2026 · 1:19 AM UTC
• Version: 1.0.3

Overview

The skill is coherent for Rocq proof work, but it tells the agent to install dependencies and run builds from downloaded theorem workspaces without enough review or isolation.

Install only if you are comfortable having the agent run opam and dune commands for theorem projects. For downloaded or third-party workspaces, review opam and dune files first and run dependency installation/builds in a disposable, least-privileged environment without sensitive credentials mounted.

A.I.G

Vulnerability Patterns

• Insecure Dependencies: Introduces malicious components through unsafe dependency sources
• Skill Instruction Hijacking: Alters the agent's session goals or safety constraints when the skill loads
• Agent Memory Poisoning: Writes attacker-controlled rules into memory that affect later sessions
• Remote Payload Retrieval and Execution: Fetches external code whose behavior can change after review
• Embedded Malicious Code: Ships malicious scripts inside the skill and executes them locally

Findings (2)

T08 · Insecure Dependencies

Error

• Location: references/proof_playbook.md:14

Finding

Untrusted Workspace Dependency Installation and Build Execution

Content

View full analysis

Vulnerability Details

File Location: references/proof_playbook.md:14-24; also present in SKILL.md:23-40,54
Vulnerability Type: Unsafe installation and execution of dependencies and build rules from an untrusted theorem workspace
Risk Level: High

Vulnerable Code Snippet:

bash

if the project has an `opam` file, install missing dependencies before proving:

opam install . --deps-only

Then confirm the workspace builds in its initial state:

dune build

Related commands in SKILL.md include:

bash

dune build

bash

opam install . --deps-only

Technical Analysis

The skill directs the agent to install dependencies and execute a build from a downloaded OpenMath theorem workspace. It does not first require validation of the workspace's opam, dune, dune-project, _CoqProject, package pins, dependency sources, or executable build actions.

An attacker-controlled workspace can influence OPAM dependency resolution through local package metadata. OPAM packages can execute build and installation commands, while Dune configurations can define actions that execute local programs or shell commands during dune build. Consequently, these instructions cross a trust boundary: data and configuration supplied by a downloaded project are treated as executable build input.

This is primarily an insecure dependency and supply-chain issue, with an additional insecure workflow configuration component. The package itself does not contain a malicious script, but its documented workflow can cause code from an untrusted workspace or dependency source to execute without sufficient review or isolation.

Attack Path

1. An attacker distributes or modifies an OpenMath theorem workspace.
2. The workspace contains a crafted opam file, malicious package pin, unsafe dependency source, or Dune build rule.
3. A user invokes this skill to prove the downloaded theorem.
4. Following the doc ...[truncated 1031 chars]

Remediation

View remediation

Remediation Suggestions

1. Require explicit review of opam, dune, dune-project, _CoqProject, package pins, source URLs, and custom build actions before executing installation or build commands.
2. Use only approved OPAM repositories and cryptographically verified or otherwise trusted package sources.
3. Pin dependencies to reviewed versions and immutable source revisions. Avoid floating branches, mutable URLs, and unreviewed local pins.
4. Run dependency installation and project builds inside a disposable, least-privileged container or virtual machine.
5. Disable or strictly limit outbound network access during builds after approved dependencies have been obtained.
6. Do not mount SSH keys, cloud credentials, package publishing tokens, browser profiles, home directories, or other sensitive host resources into the build environment.
7. Mount source files read-only where feasible and provide a dedicated output directory for generated artifacts.
8. Add a mandatory trust-boundary warning before opam install and dune build, making clear that downloaded project metadata may execute commands.
9. Prefer a two-stage workflow: inspect and resolve dependency metadata first, then execute the reviewed build in a fresh isolated environment.

other

Warning

• Location: SKILL.md:35

Finding

Incomplete Detection of Admitted Rocq Proofs

Content

View full analysis

Vulnerability Details

File Location: SKILL.md:35-40
Vulnerability Type: Incomplete proof-integrity validation
Risk Level: Medium

Vulnerable Code Snippet:

bash

dune build
grep -rn 'admit\|Admitted\.' *.v

The associated instruction states that no admit or Admitted. may remain before submission.

Technical Analysis

The validation command is not a complete check of the Rocq source tree. The shell glob *.v only selects matching files in the current directory, so proof files located in nested directories are not inspected. The pattern is also case-sensitive and does not reliably cover alternate forms such as Admit..

The skill presents this grep command as part of the proof-completion check. A clean result can therefore be interpreted as evidence that the project contains no admitted proofs even when an unchecked source file still contains an admission marker.

This is an integrity-validation weakness rather than a direct host compromise. Plain-text matching is also less reliable than semantic inspection because it may produce false positives in comments or strings and can fail to account for other project-specific mechanisms that bypass proof completion.

Attack Path

1. A theorem workspace places a relevant .v proof file in a subdirectory, or uses an admission form not matched by the case-sensitive pattern.
2. The agent runs grep -rn 'admit\|Admitted\.' *.v from the workspace root.
3. The shell passes only top-level .v files to grep, and the unmatched admission remains undetected.
4. The build succeeds because Rocq permits admitted statements.
5. The workflow treats the proof as complete and may pass it to the submission process.

Impact Assessment

Exploitation can undermine proof integrity by allowing an incomplete or unproven theorem to be treated as submission-ready. It does not directly grant operating-system privileges or arbitrary code execution. Its scope is t ...[truncated 133 chars]

Remediation

View remediation

Remediation Suggestions

1. Recursively inspect every Rocq source file rather than using a top-level *.v glob.

2. At minimum, replace the check with a recursive, case-aware command that covers all prohibited admission forms, for example:

   bash

   grep -RniE '\b(admit|admitted)\b' --include='*.v' .
   

3. Exclude generated and third-party directories only through an explicit, reviewed allowlist or denylist.

4. Prefer a Rocq-aware or AST-aware verification mechanism over plain-text grep so comments and strings do not create misleading results.

5. Enforce a project policy that rejects admitted or opaque placeholder proofs during continuous integration.

6. Verify that the theorem statement itself was not weakened or altered, in addition to checking for admission markers.

7. Run the recursive validation from a known workspace root and fail closed if no proof files are discovered or if any expected directory cannot be scanned.

SkillSpector

Vulnerability Patterns

• Prompt Injection: Instruction Override, Hidden Instructions, Exfiltration Commands
• Data Exfiltration: External Transmission, Env Variable Harvesting, File System Enumeration
• Privilege Escalation: Excessive Permissions, Sudo/Root Execution, Credential Access
• Supply Chain: Unpinned Dependencies, External Script Fetching, Obfuscated Code
• Excessive Agency: Unrestricted Tool Access, Autonomous Decision Making, Scope Creep

Findings (3)

Ae1

High

• Category: analysis-evasion
• Confidence: 100% confidence

Finding

Referenced artifact was not completely inspected

Content

Scanner excerpt · SKILL.md (reported line 20)May include surrounding context.

md

This skill package is self-contained: it consists of this `SKILL.md` plus the local `references/` files in this directory. It does not bundle or install sibling

Skill Enumeration

Medium

• Category: Agent Snooping
• Confidence: 85% confidence

Finding

Skill enumerates or reads other installed skills. Access to other skills' SKILL.md files or the skills directory reveals prompt instructions, capabilities, and secrets that should be invisible to peer skills.

Content

Scanner excerpt · SKILL.md (reported line 60)May include surrounding context.

md

- **Rocq version**: OpenMath Rocq workspaces target Rocq 9.1.0 (current stable, September 2025) with Platform 2025.08.2.
- **Companion skills**: `rocq-proof` (proving methodology, tactic reference, Ltac2), `rocq-ssreflect` (SSReflect / MathComp style), `rocq-setup` (opam, toolchain, editor), and `rocq-dune` (build system, `_CoqProject`, dune stanzas) are useful companions when already installed. Optional companions: `rocq-mwe`, `rocq-bisect`, `rocq-extraction`, `rocq-mathcomp-build`.
- **Install boundary**: This isolated skill should not instruct copying unseen `rocq-*` directories into `~/.agents/skills` or any other global skills directory. If you are installing from the full repository, review the companion skill folders there and copy them only into a deliberate project-local skills directory such as `.codex/skills` or `.claude/skills`.
- **Stdlib prefix**: Use `From Stdlib Require Import` for Rocq 9.x. The legacy `From Coq Require Import` still works with a deprecation warning; prefer `From Stdlib` for all new proofs.
- **Verification status**: A proof is complete only when `dune build` exits 0, no `admit` or `Admitted.` remains, and the LSP panel shows no errors or warnings.

Skill Enumeration

Medium

• Category: Agent Snooping
• Confidence: 85% confidence

Finding

Skill enumerates or reads other installed skills. Access to other skills' SKILL.md files or the skills directory reveals prompt instructions, capabilities, and secrets that should be invisible to peer skills.

Content

Scanner excerpt · references/companions.md (reported line 5)May include surrounding context.

md

These companion skills are optional enhancements. `openmath-rocq-theorem` must still be usable when they are absent.

Use a companion skill only if it is already installed in the active agent, or if you are working from the full repository and have explicitly reviewed and installed it into a deliberate project-local skills directory such as `.codex/skills` or `.claude/skills`.

## Common Companions

Static analysis

No suspicious patterns detected.