formal-verify

Pass

Audited by Gen Agent Trust Hub on Sep 17, 2026

Risk Level: SAFEEXTERNAL_DOWNLOADSCOMMAND_EXECUTIONDYNAMIC_EXECUTIONINDIRECT_PROMPT_INJECTION
Full Analysis
  • [EXTERNAL_DOWNLOADS]: The skill downloads the Apalache model checker from its official GitHub repository and installs standard Python dependencies (z3-solver, tree-sitter, radon, lizard, PyYAML) from PyPI. These are well-known tools necessary for the skill's formal verification and code auditing functionality.
  • [COMMAND_EXECUTION]: Orchestration scripts execute local commands for git integration, static analysis tools (radon, swiftlint), and the Apalache model checker binary to perform its auditing tasks.
  • [DYNAMIC_EXECUTION]: The skill dynamically loads tree-sitter language grammars and project-specific Python specification files from the local .verifier/ directory to execute behavioral and structural verification rules.
  • [INDIRECT_PROMPT_INJECTION]: The skill processes untrusted project files which creates a potential surface for indirect prompt injection.
  • Ingestion points: scripts/extract-facts.py reads source code (.rs, .swift) and documentation (.md) from the target project.
  • Boundary markers: No explicit prompt delimiters or 'ignore' instructions are used when presenting extracted facts to the agent.
  • Capability inventory: The skill can execute shell commands and write to the file system to generate reports and manage dependencies.
  • Sanitization: Facts are extracted via AST and regex patterns without specific filtering for malicious instructions embedded in strings or comments. The risk is considered low and inherent to the skill's primary purpose of code analysis.
Audit Metadata
Risk Level
SAFE
Analyzed
Sep 17, 2026, 01:25 PM
Security Audit — agent-trust-hub — formal-verify