By name: formal-methods description: Formal verification and static analysis — TLA+/Z3/Lean/Alloy/F*, property/mutation testing, Semgrep/CodeQL, routing.
formal methods
Category skill (blueprint pack). The description above is the only thing the
router sees — broad and generic on purpose. The fat detail lives in the
blueprints below; open the one that matches and read it in full.
Governs its own form per .claude/rules/rules-are-small-carved-sentences-pointing-to-docs.md
and .claude/rules/mirror-beacon-register-discipline.md (carved sentence = hub /
Beacon; blueprint = satellite / Mirror). The directory is an independent shipping unit.
Blueprints
tla-expert— TLA+ — operators, fairness, refinement mappings, TLC model checking, TLAPS proof discipline.z3-expert— Z3 SMT solver — F# API, sorts/constraints, quantifiers, proof obligations, tactic chains, model extraction.lean4-expert— "Lean 4 + Mathlib proofs — lake build, tactic/term-mode, abel/ring/simp, elan pinning, .olean CI caching."lean-reflection-expert— "Lean 4 metaprogramming — MetaM, TermElabM, TacticM, macro/elab_rules, Syntax/Expr pipeline, simp/reducible attributes."alloy-expert— Alloy 6 formal specs — sig/pred/fact/assert, run vs check, SAT4J, counter-examples, relational algebra, .als.fscheck-expert— FsCheck property testing — Arbitrary generators, shrink discipline, overflow-safe clamping, paper-cited algebraic laws.stryker-expert— "Stryker.NET mutation testing — score interpretation, threshold policy, operator selection, survivor triage, CI cost."semgrep-expert— Semgrep tool decisions — vs CodeQL/Roslyn, CI integration, p/ci p/secrets packs, false-positive triage, SARIF.semgrep-rule-authoring— Semgrep rule authoring — anatomy, pattern/regex/either, severity, messages, prior-review finding codification.codeql-expert— "GitHub CodeQL — query packs, custom QL, SARIF, code-scanning workflow, CWE alignment, CodeQL vs Semgrep."f-star-expert— Frefinement types — dependently-typed ML, SMT-backed refinements, Steel/Pulse, miTLS/HACL/EverParse case studies.q-sharp— Q# operator-algebra — adjointability, Pauli measurement, within/apply conjugation, Jordan-Wigner, BP/EP research lane.formal-verification-expert— Formal-verification routing — picks TLA+/Z3/Lean/Alloy/FsCheck/Stryker/Semgrep/CodeQL per property class.static-analysis-expert— Static analysis umbrella — cross-tool policy, severity baselines, warn-as-error, suppression triage, CI integration.verification-drift-auditor— Verification drift detection — audit Lean, TLA+, Z3, Semgrep against external sources for staleness and breakage.formal-analysis-gap-finder— Formal-analysis gap scanner — finds unverified invariants, unchecked consensus claims, and missing proofs.claims-tester— "Empirical claim tester — designs falsifying tests for O(n), zero-alloc, performance, and correctness claims in code."