ClawHub
Back to skill

Security audit

omega-architect-formal-proof

Security checks for vulnerabilities and agentic risk

Overview

This skill is a coherent guide for installing and using a formal proof CLI, with expected but real costs and supply-chain considerations.

Install only if you are comfortable running a research CLI from GitHub, using Lean, and potentially sending theorem prompts to an LLM provider. Pin the documented version, prefer a clean project environment, protect API keys, and start with low samples, rounds, and timeouts before larger proof searches.

A.I.G

Vulnerability Patterns
  • Skill Instruction HijackingAlters the agent's session goals or safety constraints when the skill loads
  • Agent Memory PoisoningWrites attacker-controlled rules into memory that affect later sessions
  • Remote Payload Retrieval and ExecutionFetches external code whose behavior can change after review
  • Embedded Malicious CodeShips malicious scripts inside the skill and executes them locally
  • Unauthorized Access and Privilege EscalationObtains permissions beyond the task's legitimate needs

SkillSpector

Vulnerability Patterns
  • Data ExfiltrationExternal Transmission, Env Variable Harvesting, File System Enumeration
  • Privilege EscalationExcessive Permissions, Sudo/Root Execution, Credential Access
  • Excessive AgencyUnrestricted Tool Access, Autonomous Decision Making, Scope Creep
  • Prompt InjectionInstruction Override, Hidden Instructions, Exfiltration Commands
  • Supply ChainUnpinned Dependencies, External Script Fetching, Obfuscated Code
Findings (3)

Ae4

Medium
Category
analysis-evasion
Confidence
80% confidence
Finding

Suspicious Unicode normalization or mixed-script content

Content

No source excerpt is available for this finding.

Autonomous Decision Making

Medium
Category
Excessive Agency
Confidence
75% confidence
Finding

Skill enables autonomous high-impact decisions without human-in-the-loop verification. Critical operations (destructive commands, financial transactions, data deletion) should require explicit user confirmation.

Content

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

md
## Pitfalls

1. **Prose statements do not work** — `prove` expects a Lean header (`theorem … := by`).
2. **No Lean ⇒ no verification** — generation may still run, but nothing is compiler-checked;
   check `omega status` and `lean --version` before interpreting results.
3. **Unbounded sampling is the usual budget blow-up.**
4. **`import Mathlib` is the default import set** — a narrower set compiles much faster; use

Excessive Permissions

Low
Category
Privilege Escalation
Confidence
82% confidence
Finding

The skill requests shell, file read/write, and network access, which together enable package installation, downloading code from GitHub, modifying local configuration, and invoking external tools. While these permissions are functionally aligned with installing and running a CLI, they create a meaningful attack surface if the referenced package, wheel, or remote backend is compromised or if a user runs the commands in a sensitive environment.

Content

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

md
tags: [lean4, theorem-proving, formal-verification, proof-search, mcts]
author: Li Shen
version: 1.0.3
permissions: [shell, file_read, file_write, network]
metadata:
  hermes:
    homepage: https://github.com/diamond2nv/omega-architect