The Agent Skills Directory

[CREDENTIALS_UNSAFE]: The skill contains hardcoded default credentials for ArangoDB.
In pilot_formalize.py, the variable ARANGO_PASS is hardcoded to "openSesame".
In run_formalization_benchmark.py, the ArangoDB client is initialized with username="root" and password="openSesame".
[DATA_EXFILTRATION]: The skill accesses highly sensitive authentication files.
In sanity.sh, the script reads ~/.claude/.credentials.json to verify and inspect Claude OAuth tokens, specifically extracting the expiresAt field. While used here for health checks, this provides a pathway for unauthorized access to the user's Claude account credentials.
[COMMAND_EXECUTION]: The skill performs extensive arbitrary command execution and container manipulation.
Multiple files (prove.py, extract_lemma_deps.py, ingest_prover_v1.py) use subprocess.run to execute docker exec commands, allowing for the execution of code inside containers.
prove.py calls the claude CLI using subprocess.run in a non-interactive mode.
formalize.py and full_formalize.py execute /scillm/run.sh via subprocess to generate code.
[EXTERNAL_DOWNLOADS]: The skill fetches data and scripts from remote sources.
The Dockerfile executes a remote script directly from GitHub: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash.
Multiple ingestion scripts (ingest_autoformalization.py, ingest_prover_v1.py, ingest_prover_v2.py) download datasets from HuggingFace using the datasets library.
[INDIRECT_PROMPT_INJECTION]: The skill exhibits a significant attack surface for indirect prompt injection.
Ingestion points: Natural language requirements are accepted via CLI arguments or stdin in prove.py and run.sh.
Capability inventory: The skill uses subprocess.run and docker exec to compile and execute Lean4 code generated from these requirements.
Sanitization: There is no meaningful sanitization of the input text before it is interpolated into LLM prompts in formalize.py and prove.py.

lean4-prove