Formal Methods
PassAudited by ClawScan on May 7, 2026.
Overview
This is a coherent formal-verification skill that runs local Lean, Coq, and Z3 tools; the main caveats are trusting those tools and knowing inputs are written to temporary files.
This skill appears safe and purpose-aligned for local formal verification. Before installing, make sure Lean, Coq, and Z3 come from trusted sources, avoid running untrusted proof code without review, and do not include secrets in proof or SMT inputs.
Findings (3)
Artifact-based informational review of SKILL.md, metadata, install specs, static scan signals, and capability signals. ClawScan does not execute the skill or run runtime probes.
Running the skill uses local programs and their normal search paths/runtime behavior, so untrusted proof files should be handled with the same care as other inputs to compilers or interpreters.
The skill deliberately runs local binaries on provided proof or formula files. That is central to formal verification and is disclosed, but users should recognize that execution is delegated to local prover toolchains.
This skill invokes locally installed formal verification provers via subprocess... Lean: `lean <filepath>` ... Coq: `coqc <filepath>` ... Z3: `z3 <filepath>`
Use trusted Lean/Coq/Z3 installations, keep them updated, and avoid running proof sources from untrusted origins unless you are comfortable with the local toolchain behavior.
A compromised, outdated, or unexpectedly configured local prover installation could affect the results or local execution environment.
The skill depends on user-installed external prover binaries rather than bundling or pinning them. This is normal for the stated purpose, but provenance and updates are outside the skill artifact.
`lean` ... via `elan`; `coqc` ... via `opam install coq`; `z3` ... via package manager or GitHub releases
Install the prover binaries from official sources or trusted package managers and keep them patched.
If proof files or formulas contain sensitive information, that content may be present on local temporary storage at least during execution.
The skill stores submitted proof/formula source in a local temporary directory during verification. This is purpose-aligned, but the artifacts do not describe cleanup or retention behavior.
Each invocation writes source code to a temporary directory (`os.tmpdir()/formal-methods-<hash>/`)
Avoid putting secrets in proof inputs, and clean the temporary directory if local data retention is a concern.