Leanstral Formal Verification

ReviewAudited by ClawScan on May 17, 2026.

Overview

This is a mostly coherent Lean/Mistral verification guide, but its visible verification instructions appear to run AI-generated Lean files without the safety checks they claim.

Install only if you are comfortable sending selected theorem statements and code to Mistral. Before running generated Lean files, add real proof-hole checks, verify theorem statements yourself, and run builds in a sandboxed disposable project rather than a valuable local workspace.

Findings (4)

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.

Medium

#ASI05: Unexpected Code Execution

What this means

A generated proof file could do more than prove a theorem when built locally, potentially affecting files or the local Lean project.

Why it was flagged

The skill acknowledges generated Lean files are untrusted, then the visible template compiles them with `lake build`. That is central to verification, but it needs strong containment because generated Lean files may execute elaboration/evaluation behavior during build.

Skill content

Generated `.lean` files are untrusted code ...
cp "$1" "$PROJECT_DIR/Proof.lean"
cd "$PROJECT_DIR"
lake build

Recommendation

Review generated `.lean` files before building them, run verification in a disposable sandbox or container, and restrict filesystem/network access where possible.

Medium

#ASI09: Human-Agent Trust Exploitation

What this means

Users may believe a passing build proves the intended property even if proof holes remain or the build was not actually isolated.

Why it was flagged

The visible script does not show any check that rejects `sorry` or `admit`, and merely changing into a project directory is not isolation. This overstates the safety and assurance provided by the template.

Skill content

`verify.sh` rejects proof holes (`sorry`/`admit`) and compiles in an isolated project directory.
...
cp "$1" "$PROJECT_DIR/Proof.lean"
cd "$PROJECT_DIR"
lake build

Recommendation

Add explicit `sorry`/`admit` rejection, treat warnings as failures, verify theorem statements manually, and document the actual isolation method if one is required.

Low

#ASI03: Identity and Privilege Abuse

What this means

The skill can use your Mistral account quota and access through the API key.

Why it was flagged

The skill requires a provider API key to call Mistral. This is expected for the stated integration and no artifact shows hardcoding, logging, or unrelated use of the key.

Skill content

Required env vars: MISTRAL_API_KEY; Primary credential: MISTRAL_API_KEY

Recommendation

Use a dedicated API key where possible, keep it out of prompts and files, and revoke or rotate it if exposed.

Low

#ASI07: Insecure Inter-Agent Communication

What this means

Any code or protocol details included in prompts may be sent to Mistral.

Why it was flagged

The artifact discloses that user-supplied theorem statements and code are transmitted to an external provider. This is purpose-aligned and clearly warned, but it is still a sensitive data boundary.

Skill content

Theorem statements and code are sent to Mistral's API. Do not include confidential code, secrets, or proprietary protocol details in prompts.

Recommendation

Do not submit secrets, proprietary code, or sensitive protocol details unless your organization permits that provider use.