ClawHub
Back to skill

Security audit

Leanstral Formal Verification

Security checks for vulnerabilities and agentic risk

Overview

The skill is mostly coherent, but it gives unsafe and overstated verification instructions for compiling untrusted model-generated Lean code on the user's host machine.

Review this skill carefully before installing. Its Mistral API use is expected for Leanstral, but do not send private code or secrets. More importantly, do not compile model-generated Lean files with the provided verify.sh on a normal project or shell; use a disposable, isolated environment and verify that the exact generated file is checked and proof holes are rejected.

A.I.G

Vulnerability Patterns
  • Insecure Skill Coding PracticesFinds exploitable flaws such as hardcoded secrets or command injection
  • 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
Findings (1)

T09 · Insecure Skill Coding Practices

Error
Location
SKILL.md:29
Finding

Untrusted Model-Generated Lean Code Is Compiled Without the Claimed Isolation and Proof-Hole Checks

Content
View full analysis
" cp "$1" "$PROJECT_DIR/Proof.lean" cd "$PROJECT_DIR" lake build ``` ### Technical Analysis The Skill directs users to send theorem statements and code to an external model and then compile the returned Lean source. Although the documentation correctly identifies generated `.lean` files as untrusted, the supplied `verify.sh` does not implement its stated security controls: 1. It contains no check that rejects `sorry`, `admit`, or equivalent proof-bypassing constructs. 2. `cd "$PROJECT_DIR"` only changes the working directory; it does not create a security sandbox or isolate the process. 3. `lake build` runs with the invoking user's permissions, environment, filesystem access, and network access. 4. Lean supports compile-time metaprogramming and elaboration features. Consequently, compiling untrusted Lean source is not equivalent to parsing inert proof text. 5. The script copies the input over `Proof.lean`, potentially replacing an existing project file. 6. Plain `lake build` does not necessarily prove that the newly copied `Proof.lean` is a configured build target. The command may therefore succeed without validating the intended file. The flagged pipeline at line 454 is not itself a remote shell execution pipeline: ```bash cur ...[truncated 2022 chars]
Remediation
View remediation

SkillSpector

Vulnerability Patterns
  • Data ExfiltrationExternal Transmission, Env Variable Harvesting, File System Enumeration
  • Supply ChainUnpinned Dependencies, External Script Fetching, Obfuscated Code
  • Trigger AbuseOverly Broad Trigger, Shadow Command Trigger, Keyword Baiting Trigger
  • Prompt InjectionInstruction Override, Hidden Instructions, Exfiltration Commands
  • Privilege EscalationExcessive Permissions, Sudo/Root Execution, Credential Access
Findings (8)

External Script Fetching

High
Category
Supply Chain
Confidence
90% confidence
Finding

Remote code is downloaded and executed. This bypasses code review and could introduce malicious code.

Content

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

md
# Basic retry loop: try up to 3 times, stop on first success
for i in 1 2 3; do
  echo "Attempt $i..."
  curl -s ... | python3 -c "import sys,json; print(json.load(sys.stdin)['choices'][0]['message']['content'])" > proof.lean
  if bash verify.sh proof.lean 2>/dev/null; then
    echo "✅ Proof verified on attempt $i"
    break

Vague Triggers

Medium
Category
Not specified by scanner
Confidence
91% confidence
Finding

The manifest trigger list includes generic phrases such as "formal proof", "mathematical proof", and especially "code verification" and "correctness proof", which can plausibly appear in ordinary development discussions outside the narrow Leanstral/Lean 4 context. The description states use cases broadly but does not provide exclusion conditions or negative examples to constrain when the skill should or should not activate from those phrases alone.

Content

No source excerpt is available for this finding.

External Transmission

Medium
Category
Data Exfiltration
Confidence
50% confidence
Finding

Data is being sent to an external URL. This could be legitimate telemetry or data exfiltration. Manual review is recommended.

Content

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

md
| Context length | 256K tokens |
| License | Apache 2.0 (open weights) |
| API model ID | `labs-leanstral-2603` |
| API base URL | `https://api.mistral.ai/v1` |

### Why Leanstral beats general-purpose LLMs at proofs

External Transmission

Medium
Category
Data Exfiltration
Confidence
96% confidence
Finding

The explicit curl example uses a bearer token and transmits prompt content to a third-party service. In the context of a verification skill, prompts are likely to contain code and formalized security properties, which may be highly sensitive even if not traditionally classified as secrets.

Content

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

The primary way to use this skill: call the Mistral API directly.

bash
curl -X POST "https://api.mistral.ai/v1/chat/completions" \
  -H "Authorization: Bearer $MISTRAL_API_KEY" \
  -H "Content-Type: application/json" \
  -d '{

External Transmission

Medium
Category
Data Exfiltration
Confidence
96% confidence
Finding

The explicit curl example uses a bearer token and transmits prompt content to a third-party service. In the context of a verification skill, prompts are likely to contain code and formalized security properties, which may be highly sensitive even if not traditionally classified as secrets.

Content

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

The primary way to use this skill: call the Mistral API directly.

bash
curl -X POST "https://api.mistral.ai/v1/chat/completions" \
  -H "Authorization: Bearer $MISTRAL_API_KEY" \
  -H "Content-Type: application/json" \
  -d '{

External Transmission

Medium
Category
Data Exfiltration
Confidence
95% confidence
Finding

The Python example configures a client to send user content to the Mistral API, again creating a real external data exposure path. Because this is sample code intended for direct reuse, it meaningfully operationalizes transmission of potentially sensitive code or specifications.

Content

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

md
client = OpenAI(
    api_key="***",
    base_url="https://api.mistral.ai/v1"
)

response = client.chat.completions.create(

External Transmission

Medium
Category
Data Exfiltration
Confidence
97% confidence
Finding

This concrete shell snippet automates repeated uploads to the external API and writes returned model output into local proof files. The main risk is not the local file write but the repeated third-party transmission of possibly confidential proof requests, source code, and protocol descriptions.

Content

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

bash
for i in 1 2 3; do
  curl -s -X POST "https://api.mistral.ai/v1/chat/completions" \
    -H "Authorization: Bearer $MISTRAL_API_KEY" \
    -H "Content-Type: application/json" \
    -d "{\"model\":\"labs-leanstral-2603\",\"temperature\":1.0,\"max_tokens\":32000,\"messages\":[{\"role\":\"user\",\"content\":\"$(cat proof_request.txt | jq -Rs .)\"}]}" \

External Transmission

Medium
Category
Data Exfiltration
Confidence
97% confidence
Finding

This concrete shell snippet automates repeated uploads to the external API and writes returned model output into local proof files. The main risk is not the local file write but the repeated third-party transmission of possibly confidential proof requests, source code, and protocol descriptions.

Content

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

bash
for i in 1 2 3; do
  curl -s -X POST "https://api.mistral.ai/v1/chat/completions" \
    -H "Authorization: Bearer $MISTRAL_API_KEY" \
    -H "Content-Type: application/json" \
    -d "{\"model\":\"labs-leanstral-2603\",\"temperature\":1.0,\"max_tokens\":32000,\"messages\":[{\"role\":\"user\",\"content\":\"$(cat proof_request.txt | jq -Rs .)\"}]}" \

Static analysis

No suspicious patterns detected.