The Agent Skills Directory

[SAFE]: No security issues detected. The skill implements a program-to-specification transformer using standard Python libraries. Analysis of the scripts confirms that they perform static analysis rather than code execution.- [INDIRECT_PROMPT_INJECTION]: Analyzed as a potential surface. The skill ingests untrusted source code which is a standard operation for its purpose. Ingestion points: The ProgramAnalyzer in scripts/program_analyzer.py reads user-provided source files. Boundary markers: No explicit delimiters are added to the output to isolate potentially malicious comments in the generated TLA+ spec. Capability inventory: The skill writes generated TLA+ files to the local filesystem (scripts/generate_spec.py). Sanitization: The skill uses ast.parse and regular expressions to extract structure, avoiding execution of the input code. This surface is considered safe given the tool's intended use case for formal verification.- [DATA_EXPOSURE]: Analyzed as a potential surface. The skill reads from and writes to paths provided by the user via command-line arguments. No hardcoded sensitive paths (e.g., SSH keys or cloud credentials) were found in the codebase.

tlaplus-spec-generator