verified-pseudocode-extractor
Installation
SKILL.md
Verified Pseudocode Extractor
The reverse of → python-to-dafny-translator. You have verified code; you want to carry the verification obligations into a reimplementation without carrying the verification language.
The output is pseudocode annotated with preconditions, postconditions, and invariants — so whoever implements it knows exactly what the verifier was relying on.
What to keep vs drop
| Dafny/Lean/TLA+ construct | In pseudocode |
|---|---|
requires P |
KEEP — // PRE: P |
ensures Q |
KEEP — // POST: Q |
invariant I (loop) |
KEEP — // INV: I at loop head |
decreases e |
KEEP — // TERMINATES BY: e decreases each iteration |
ghost var |
DROP from code, KEEP as comment explaining what it tracks |
assert P (proof hint) |
Usually DROP — it's a verifier hint, not a runtime check |
lemma calls |
DROP — they have no runtime effect |
modifies clauses |
KEEP as comment — tells implementer what's mutated |