Formal Methods

• Analyzed: May 11, 2026, 5:54 AM
• Findings: 1
• Version: 1.0.8
• Hash: 477b3caa832b6deeb54bd90bce06175ca215cd2b1d05e8dce1694bdc0def6dcf
• Source: palm
• External report: View on VirusTotal

Findings (1)

The skill bundle provides tools for formal verification (Lean 4, Coq, Z3) that execute code via subprocesses. While the intent appears benign and aligned with academic use, the skill is classified as suspicious due to a potential shell injection vulnerability: the `lean_check`, `coq_check`, and `coq_compile` tools in `SKILL.md` accept a user-defined `filename` parameter that is directly interpolated into shell commands (e.g., `lean <filepath>`). Without explicit evidence of input sanitization in the provided documentation, this design poses a risk of arbitrary command execution if an attacker can influence the filename or code content.