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`