formal-verify

Pass

Audited by Gen Agent Trust Hub on Apr 13, 2026

Risk Level: SAFEEXTERNAL_DOWNLOADSREMOTE_CODE_EXECUTIONCOMMAND_EXECUTIONPROMPT_INJECTION
Full Analysis
  • [EXTERNAL_DOWNLOADS]: The scripts/install-deps.sh script downloads the Apalache model checker from its official GitHub repository to handle behavioral state-machine verification.
  • [REMOTE_CODE_EXECUTION]: The scripts/verify-behavioral.py script dynamically loads and executes Python modules from the project's .verifier/specs/ directory using importlib, allowing user-defined Z3Py specifications to run during the verification process.
  • [COMMAND_EXECUTION]: Multiple components use the subprocess module to execute system commands for source code fact extraction (Git), complexity auditing (Radon), and running the Apalache model checker.
  • [PROMPT_INJECTION]: The skill processes untrusted source code and specification files from a project directory, creating a surface for indirect prompt injection if the agent is instructed to process a malicious repository.
Audit Metadata
Risk Level
SAFE
Analyzed
Apr 13, 2026, 08:36 AM