CtrlK
BlogDocsLog inGet started
Tessl Logo

verified-pseudocode-extractor

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.

Install with Tessl CLI

npx tessl i github:santosomar/general-secure-coding-agent-skills --skill verified-pseudocode-extractor
What are skills?

90

Quality

88%

Does it follow best practices?

Impact

Pending

No eval scenarios have been run

SKILL.md
Review
Evals

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+ constructIn pseudocode
requires PKEEP — // PRE: P
ensures QKEEP — // POST: Q
invariant I (loop)KEEP — // INV: I at loop head
decreases eKEEP — // TERMINATES BY: e decreases each iteration
ghost varDROP 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 callsDROP — they have no runtime effect
modifies clausesKEEP as comment — tells implementer what's mutated

The annotation rule

Every dropped verification construct becomes a comment at the point where the verifier used it. Don't aggregate them into a docblock at the top — put the invariant comment at the loop head, where it's checked.

Worked example — Dafny → annotated pseudocode

Dafny (verified):

method BinarySearch(a: array<int>, key: int) returns (idx: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]   // sorted
  ensures 0 <= idx ==> idx < a.Length && a[idx] == key
  ensures idx < 0  ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant forall i :: 0 <= i < lo ==> a[i] < key
    invariant forall i :: hi <= i < a.Length ==> a[i] > key
    decreases hi - lo
  {
    var mid := lo + (hi - lo) / 2;
    if a[mid] < key      { lo := mid + 1; }
    else if a[mid] > key { hi := mid; }
    else                 { return mid; }
  }
  return -1;
}

Extracted pseudocode:

function binary_search(a: sorted array of int, key: int) -> int
    // PRE:  a is sorted ascending (a[i] <= a[j] for i < j)
    // POST: if result >= 0 then a[result] == key
    // POST: if result < 0  then key is not in a

    lo ← 0
    hi ← length(a)

    while lo < hi:
        // INV: 0 <= lo <= hi <= length(a)
        // INV: everything left of lo is < key   (a[0..lo) all < key)
        // INV: everything at/right of hi is > key   (a[hi..) all > key)
        // TERMINATES BY: (hi - lo) strictly decreases each iteration

        mid ← lo + (hi - lo) / 2        // no overflow — NOT (lo+hi)/2

        if a[mid] < key:
            lo ← mid + 1
        else if a[mid] > key:
            hi ← mid
        else:
            return mid

    return -1

What got preserved: The three loop invariants are the essence of why binary search works. An implementer who maintains them can't get the algorithm wrong. The overflow note on mid — that's from the verified lo + (hi - lo) / 2, not the naive (lo + hi) / 2.

What got dropped: Nothing here — this Dafny had no ghost state or lemmas. If it had ghost var numCompares, that'd become a comment: // (verifier tracked comparison count for complexity proof — not needed at runtime).

From TLA+

TLA+ → pseudocode is different: TLA+ actions become pseudocode steps, and the invariant becomes a global assertion.

// GLOBAL INVARIANT (must hold after every step):
//   at most one process in critical section

step AcquireLock(p):
    // ENABLED WHEN: lock is free
    wait until lock == FREE
    lock ← p

step ReleaseLock(p):
    // ENABLED WHEN: p holds the lock
    assert lock == p
    lock ← FREE

The ENABLED WHEN annotations are the TLA+ guards. They tell the implementer: this operation blocks (or fails) if the condition isn't met.

Do not

  • Do not drop the invariants. They're the whole point. Pseudocode without the invariants is just unverified pseudocode.
  • Do not translate ghost variables into runtime variables. They existed only to state the proof. Mentioning them in comments is fine; computing them is waste.
  • Do not simplify the pseudocode in ways the verifier would reject. (lo + hi) / 2 is simpler than lo + (hi - lo) / 2 and also wrong at scale. Keep what the verifier verified.
  • Do not lose the decreases clause. Termination is a correctness property. "This loop terminates because X decreases" belongs in the output.

Output format

## Source
<Dafny | Lean | TLA+> — <file/module>

## Verified properties
PRE:  <list>
POST: <list>
INV:  <per-loop list>
TERM: <decreases measures>

## Pseudocode
<annotated pseudocode — annotations inline at point-of-use>

## Dropped constructs
<ghost vars, lemmas, proof hints — what they were for>

## Implementation warnings
<anything the verifier relied on that a naive implementer might get wrong — overflow, aliasing, atomicity>
Repository
santosomar/general-secure-coding-agent-skills
Commit

47d56bb

Last updated
Created

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.

Claim skill