ClawHub
Back to skill

Security audit

omega-architect-formal-proof

Security checks for vulnerabilities and agentic risk

Overview

This skill is a disclosed formal proof workflow helper that installs and runs a Lean/omega-architect CLI, with no hidden persistence, exfiltration, or unrelated behavior found.

Install only if you are comfortable running a third-party proof-search CLI from GitHub and potentially using API keys or local model resources. Pin versions where possible, verify the upstream project and release artifacts, start with low sample and round limits, and treat only Lean-compiled proofs as verified.

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

Autonomous Decision Making

Medium
Category
Excessive Agency
Content
## 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
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.

Excessive Permissions

Low
Category
Privilege Escalation
Content
tags: [lean4, theorem-proving, formal-verification, proof-search, mcts]
author: Li Shen
version: 1.0.2
permissions: [shell, file_read, file_write, network]
metadata:
  hermes:
    homepage: https://github.com/diamond2nv/omega-architect
Confidence
76% confidence
Finding
The skill requests shell, file_read, file_write, and network permissions, which together enable downloading and installing code from remote repositories, modifying local configuration, and executing external tooling. While these capabilities are functionally relevant for installing omega-architect and Lean, they create a substantial attack surface if the skill is invoked on untrusted inputs or pinned dependencies are compromised.

Static analysis

No suspicious patterns detected.