santosomar/formal-spec-generator
skills/verification/formal-spec-generator/SKILL.md
Dispatch skill — routes a formal specification request to the right concrete generator based on what's being specified and what needs to be proven. Use when the user asks to formally specify something without naming a target formalism, or when unsure which verification tool fits the problem.
tools
Updated Apr 13, 2026
$ install --global
skillsauthnpx skillsauth add santosomar/general-secure-coding-agent-skills formal-spec-generatorInstall this skill globally with one command. Works with Claude Code, Cursor, and Windsurf.
Security Scan Results
3 of 9 scanners reported clean
Some scanners were skipped, did not run, or reported a non-clean status. Review each row below.
3
Scanners Passed
9
Scanners in report
Clean
TrivyContainer and dependency vulnerability scanner
95%
Clean
SemgrepStatic code analysis for vulnerabilities
95%
Clean
mcp-scan (Snyk)Model Context Protocol security validation
95%
Skipped
Snyk (dep)Open source security scanning
50%
Skipped
Socket.devSupply chain security analysis
50%
Skipped
VirusTotalMulti-engine malware detection
50%
Skipped
CrowdStrikeAdvanced threat intelligence
50%
Skipped
OSV-ScannerOpen Source Vulnerability database check
50%
Skipped
OWASP Dep-Check
50%
Last scanned: Apr 13, 2026, 4:39 AM42.4s1 file scanned
SKILL.md
- name:
- formal-spec-generator
- description:
- Dispatch skill — routes a formal specification request to the right concrete generator based on what's being specified and what needs to be proven. Use when the user asks to formally specify something without naming a target formalism, or when unsure which verification tool fits the problem.
- license:
- Apache-2.0
- category:
- verification
- suite:
- general-secure-coding-agent-skills
- version:
- 0.3.0
- related:
- python-to-dafny-translator, program-to-tlaplus-spec-generator, specification-to-temporal-logic-generator
Formal Spec Generator
This is a dispatch skill. It doesn't generate specs itself — it picks the right specialized generator based on what you're trying to verify.
Dispatch table
| You have | You want to prove | → Go to |
| ------------------------------------------- | -------------------------------------- | ------------------------------------------------ |
| A Python function | It computes the right answer | → python-to-dafny-translator |
| A C/C++ function | No overflow, no OOB, correct result | → cpp-to-dafny-translator |
| Python/C++, Dafny can't prove it automatically | Deep mathematical property | → python-to-lean4-translator / → c-cpp-to-lean4-translator |
| Concurrent/distributed code | No race, no deadlock, protocol correctness | → program-to-tlaplus-spec-generator |
| Hardware-adjacent / embedded state machine | Reachability, CTL branching properties | → smv-model-extractor |
| A natural-language requirement | A checkable property (any formalism) | → requirement-to-tlaplus-property-generator or → specification-to-temporal-logic-generator |
| A loop that Dafny can't verify | The loop invariant | → invariant-inference / → abstract-invariant-generator |
Three questions that route you
-
Is it sequential or concurrent?
- Sequential → Dafny / Lean (prove a function correct)
- Concurrent → TLA+ / SMV (prove an interleaving safe)
-
Is the state space finite?
- Finite, small → SMV (explicit-state, fast, CTL)
- Finite, large → TLA+ with TLC (explicit-state, more expressive)
- Infinite → Dafny / Lean (symbolic, per-function)
-
Do you need automation or a proof artifact?
- "Just tell me if it's right" → Dafny (SMT-backed, mostly automatic)
- "I need the proof itself" → Lean (interactive, proof term is the output)
Common misroutings
| You asked for | But you actually need |
| ------------------------------------- | ----------------------------------------------------------- |
| "Verify this sorting function" → TLA+ | Dafny. TLA+ is for concurrency, not algorithmic correctness. |
| "Prove no deadlock" → Dafny | TLA+. Dafny is sequential; deadlock is a concurrency property. |
| "Check this protocol" → Lean | TLA+ first. Lean proofs of protocols are PhD theses. Model-check first. |
| "Formally specify this API" → any | Probably not formal methods at all — → api-design-assistant. "Formal" often just means "written down carefully." |
Do not
- Do not reach for the heaviest tool first. Model checking (TLA+/SMV) is orders of magnitude less effort than theorem proving (Lean). Try the cheap thing.
- Do not formally verify what you can adequately test. Formal methods pay off when the input space is adversarial or infinite. For
parse_date(), write more tests.
Related Skills
santosomar/verified-pseudocode-extractor
development
VerifiedTrustedCommunity
Extracts human-readable pseudocode from a verified formal artifact (Dafny, Lean, TLA+) while preserving the verified properties as annotations, so the proof-carrying logic can be reimplemented in a production language. Use when porting verified code to an unverified target, when documenting what a formal spec actually does, or when handing a verified algorithm to an implementer.
SKILL.mdUpdated Apr 13, 2026
santosomar/tlaplus-spec-generator
development
VerifiedTrustedCommunity
Translates natural-language or pseudocode descriptions of concurrent and distributed systems into TLA+ specifications ready for the TLC model checker. Identifies state variables, actions, type invariants, safety properties, and liveness properties from the description. Use when formalizing a protocol, when the user describes a distributed algorithm to verify, when designing a consensus or locking scheme, or when starting formal verification of a concurrent system.
SKILL.mdUpdated Apr 13, 2026
santosomar/tlaplus-model-reduction
testing
VerifiedTrustedCommunity
Reduces a TLA+ model so TLC can actually check it — shrinks constants, adds state constraints, abstracts data, or applies symmetry — when the state space is too large to enumerate. Use when TLC runs out of memory, when checking takes hours, or when a spec works at N=2 and you need confidence at larger scale.
SKILL.mdUpdated Apr 13, 2026
santosomar/tlaplus-guided-code-repair
development
VerifiedTrustedCommunity
TLA+-specific instance of model-guided repair — reads a TLC error trace, identifies the enabling condition that should have been false, strengthens the corresponding action, and maps the fix to source code. Use when TLC reports an invariant violation or deadlock and you have the code-to-TLA+ mapping from extraction.
SKILL.mdUpdated Apr 13, 2026