The Agent Skills Directory

[COMMAND_EXECUTION]: The skill invokes sibling tool scripts (memory, interview, lean4-prove) using subprocess.run with argument lists. This method avoids shell interpretation of user-provided strings, mitigating command injection risks. Evidence: subprocess.run([MEMORY_RUN] + [str(a) for a in args], ...) in formalize.py.\n- [REMOTE_CODE_EXECUTION]: Logic from the lean4-prove sibling skill is imported at runtime by modifying sys.path. This is a localized integration pattern within the authorized skill ecosystem for retrieving similar proofs. Evidence: sys.path.insert(0, str(LEAN4_PROVE_SKILL)) in formalize.py.\n- [PROMPT_INJECTION]: The skill processes user-supplied natural language requests, creating an ingestion point for potential indirect injection. However, its function is to clarify intent through a structured loop, limiting the risk of malicious instructions reaching downstream tools. Ingestion point: request parameter in formalize.py. Boundary markers: Absent. Capability inventory: Subprocess calls and temporary file creation. Sanitization: Regex pattern matching.

formalize-request