formal-verification-guide
Installation
SKILL.md
Formal Verification Guide
A skill for applying formal methods to verify software and hardware correctness. Covers model checking, interactive theorem proving, specification languages, and practical verification workflows used in systems and programming language research.
Verification Approaches Overview
Methods Comparison
| Approach | Technique | Strengths | Limitations |
|---|---|---|---|
| Model checking | Exhaustive state exploration | Fully automatic, produces counterexamples | State space explosion |
| Theorem proving | Interactive proof construction | Handles infinite state | Requires expert effort |
| Abstract interpretation | Sound static analysis | Automatic, scales well | May report false positives |
| SMT solving | Constraint satisfiability | Powerful automation | Limited to decidable theories |
| Runtime verification | Execution monitoring | Low barrier, practical | Only checks observed runs |