New: 97,000+ skills indexed from GitHub repos with 100+ stars · every skill safety-checkedBrowse top skillsTop skills
Esc to closeBrowse all skills
Submit a skillBrowse skills
Submit a skillBrowse skills

Agent skill

Python To Dafny Translator

by ArabelaTso in ArabelaTso/Skills-4-SE

Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable.

Apache-2.0Auto-check passedWriting & Content

Install Python To Dafny Translator

skills CLI
$ npx skills add ArabelaTso/Skills-4-SE --skill python-to-dafny-translator -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI
$ gh skill install ArabelaTso/Skills-4-SE python-to-dafny-translator --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy
$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .claude/skills && cp -r skills-src/skills/python-to-dafny-translator .claude/skills/python-to-dafny-translator && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Facts

Skill name
python-to-dafny-translator
GitHub stars
253
Token cost
~3.1k tokens
SKILL.md length
760 words
Files
2 (incl. references)
Skills in repo
151
Repo updated
First seen
Licence
Apache-2.0

At a glance

Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable.

  • Works in 6 steps: Analyze Python Code → Design Dafny Structure → Translate Code → …
  • The user asks to convert Python code to Dafny
  • SKILL.md covers Overview, Translation Workflow, Common Translation Patterns and Examples, plus 4 more sections
  • Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Python To Dafny Translator is an agent skill from ArabelaTso/Skills-4-SE. Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable. Use when the user asks to convert Python code to Dafny, port Python programs to Dafny, add formal verification to Python code, or create Dafny versions of Python algorithms with specifications.

Its SKILL.md is about 3.1k tokens, which your agent loads only when the skill is triggered. The skill folder holds 2 other files, including reference files (for example `references/translation_patterns.md`).

It sits in Writing & Content, covering Translation. It works with Python. The repository describes itself as: A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows. The licence is Apache-2.0.

When your agent uses it

  • The user asks to convert Python code to Dafny
  • Port Python programs to Dafny
  • Add formal verification to Python code
  • Create Dafny versions of Python algorithms with specifications

Example prompts

  • “/python-to-dafny-translator”

Requirements

  • Python 3

Workflow steps

6 steps, taken from the step headings in SKILL.md.

  1. Analyze Python Code
  2. Design Dafny Structure
  3. Translate Code
  4. Add Specifications
  5. Verify and Test
  6. Refine and Optimize

What it can do on your machine

Read from SKILL.md and the folder at commit 4f38503. It shows what the files ask for, not the result of running them.

  • Tool permissions

    Pre-approves nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.

    From allowed-tools in the SKILL.md frontmatter.

  • Runs code

    No scripts in the folder and no shell commands in SKILL.md (its code samples are dafny, python and bash).

    From the folder's file list and the shell code blocks in SKILL.md.

  • Network

    Links to these hosts (documentation or services it may open):

    • dafny.org

    From URLs in SKILL.md, links to its own repository left out.

  • Credentials

    Names no API keys, tokens, secrets or passwords.

    From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Python To Dafny Translator loads about 3.1k tokens when it runs, and up to ~5.9k if it reads all its reference files. Until then it costs about 95 tokens; SKILL.md has 760 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it
~95
When it runs · the whole SKILL.md, loaded when a task matches
~3.1k
With references · SKILL.md plus every file in references/, read only if the agent opens them
~5.9k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check passed

The automated check found no risky patterns in SKILL.md.

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from ArabelaTso/Skills-4-SE at commit 4f38503, republished under its Apache-2.0 licence (© ArabelaTso). 760 words, ~3,145 tokens.

Download SKILL.mdSave it as .claude/skills/python-to-dafny-translator/SKILL.md (or your agent's skills folder). This skill also uses 1 other file; get the full folder from GitHub.
name
python-to-dafny-translator
description
Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable. Use when the user asks to convert Python code to Dafny, port Python programs to Dafny, add formal verification to Python code, or create Dafny versions of Python algorithms with specifications.

Python to Dafny Translator

Overview

Transform Python programs into equivalent Dafny code that preserves the original semantics while adding formal specifications and leveraging Dafny's verification capabilities.

Translation Workflow

Step 1: Analyze Python Code

Understand the Python program structure and semantics:

  1. Identify program components:

    • Functions and their signatures
    • Classes and methods
    • Data structures (lists, dicts, sets)
    • Control flow (loops, conditionals)
    • Variable types (infer from usage)

  2. Understand semantics:

    • What does the program compute?
    • What are the inputs and outputs?
    • What are the preconditions and postconditions?
    • Are there invariants or constraints?

  3. Note translation challenges:

    • Dynamic typing
    • Mutable data structures
    • Exception handling
    • Python-specific features (list comprehensions, generators)
Step 2: Design Dafny Structure

Plan the Dafny equivalent:

  1. Choose appropriate types:

    • int for integers (arbitrary precision)
    • nat for non-negative integers
    • bool for booleans
    • string for strings
    • real for floating-point (when needed)
    • seq<T> for lists
    • set<T> for sets
    • map<K, V> for dictionaries
    • array<T> for mutable arrays

  2. Determine function vs method:

    • Function: Pure computation, no side effects, used in specifications
    • Method: Can have side effects, modify state, perform I/O

  3. Plan specifications:

    • Preconditions (requires)
    • Postconditions (ensures)
    • Loop invariants
    • Frame conditions (modifies, reads)
Step 3: Translate Code

Follow these translation principles:

Functions

Pattern: Pure function

python
# Python
def add(a, b):
    return a + b
dafny
// Dafny
function add(a: int, b: int): int
{
    a + b
}

Pattern: Function with specifications

python
# Python
def max_value(a, b):
    """Returns the maximum of a and b"""
    return a if a > b else b
dafny
// Dafny
function max(a: int, b: int): int
    ensures max(a, b) >= a && max(a, b) >= b
    ensures max(a, b) == a || max(a, b) == b
{
    if a > b then a else b
}
Methods

Pattern: Method with side effects

python
# Python
def increment_counter(counter):
    counter[0] += 1
dafny
// Dafny
method incrementCounter(counter: array<int>)
    requires counter.Length > 0
    modifies counter
    ensures counter[0] == old(counter[0]) + 1
{
    counter[0] := counter[0] + 1;
}
Control Flow

Pattern: If-else

python
# Python
def abs_value(x):
    if x < 0:
        return -x
    else:
        return x
dafny
// Dafny
function abs(x: int): int
    ensures abs(x) >= 0
{
    if x < 0 then -x else x
}

Pattern: For loop → While loop with invariants

python
# Python
def sum_array(arr):
    total = 0
    for i in range(len(arr)):
        total += arr[i]
    return total
dafny
// Dafny
method sumArray(arr: array<int>) returns (total: int)
{
    total := 0;
    var i := 0;
    while i < arr.Length
        invariant 0 <= i <= arr.Length
        invariant total == sum(arr[..i])
    {
        total := total + arr[i];
        i := i + 1;
    }
}

function sum(s: seq<int>): int
{
    if |s| == 0 then 0 else s[0] + sum(s[1..])
}
Collections

Pattern: Lists → Sequences

python
# Python
lst = [1, 2, 3, 4, 5]
first = lst[0]
length = len(lst)
dafny
// Dafny
var lst: seq<int> := [1, 2, 3, 4, 5];
var first: int := lst[0];
var length: int := |lst|;

Pattern: Dictionaries → Maps

python
# Python
d = {"a": 1, "b": 2}
value = d["a"]
dafny
// Dafny
var d: map<string, int> := map["a" := 1, "b" := 2];
var value: int := d["a"];
Classes

Pattern: Simple class

python
# Python
class Point:
    def __init__(self, x, y):
        self.x = x
        self.y = y

    def move(self, dx, dy):
        self.x += dx
        self.y += dy
dafny
// Dafny
class Point {
    var x: int
    var y: int

    constructor(x: int, y: int)
        ensures this.x == x && this.y == y
    {
        this.x := x;
        this.y := y;
    }

    method move(dx: int, dy: int)
        modifies this
        ensures x == old(x) + dx
        ensures y == old(y) + dy
    {
        x := x + dx;
        y := y + dy;
    }
}
Step 4: Add Specifications

Enhance the Dafny code with formal specifications:

  1. Preconditions (requires):

    • What must be true before the function/method executes?
    • Example: requires n >= 0 for factorial

  2. Postconditions (ensures):

    • What is guaranteed after execution?
    • Example: ensures result >= 0 for absolute value

  3. Loop invariants:

    • What is true at the start of each iteration?
    • Example: invariant 0 <= i <= n for loop counter

  4. Frame conditions:

    • modifies: What can be modified?
    • reads: What can be read?
Step 5: Verify and Test

Ensure the translated code is correct:

  1. Run Dafny verifier:

    bash
    dafny verify program.dfy

  2. Fix verification errors:

    • Add missing invariants
    • Strengthen postconditions
    • Add helper lemmas if needed

  3. Test execution:

    bash
    dafny run program.dfy

  4. Compare outputs:

    • Run original Python program
    • Run translated Dafny program
    • Verify outputs match
Step 6: Refine and Optimize

Improve the translated code:

  1. Simplify specifications:

    • Remove redundant conditions
    • Use helper functions for complex specs

  2. Add documentation:

    dafny
    // Computes the factorial of n
function factorial(n: nat): nat

  3. Optimize for verification:

    • Break complex functions into smaller pieces
    • Add intermediate assertions
    • Use lemmas for complex proofs

Common Translation Patterns

For detailed patterns, see translation_patterns.md.

Quick Reference
PythonDafny
x = 10var x: int := 10;
def f(x):function f(x: int): int or method f(x: int)
return xx (function) or return x; (method)
if x > 0:if x > 0 then or if x > 0 {
for i in range(n):while i < n with invariants
[1, 2, 3][1, 2, 3] (seq)
{1, 2, 3}{1, 2, 3} (set)
{"a": 1}map["a" := 1]
len(lst)|lst|
lst[i]lst[i]
class C:class C {
NoneUse Option<T> datatype
Show full SKILL.md (277 more words)Show less

Examples

Example 1: Simple Function

Python Input:

python
def factorial(n):
    if n <= 1:
        return 1
    return n * factorial(n - 1)

Dafny Output:

dafny
function factorial(n: nat): nat
    ensures factorial(n) >= 1
{
    if n <= 1 then 1
    else n * factorial(n - 1)
}
Example 2: Array Processing

Python Input:

python
def find_max(arr):
    if len(arr) == 0:
        return None
    max_val = arr[0]
    for i in range(1, len(arr)):
        if arr[i] > max_val:
            max_val = arr[i]
    return max_val

Dafny Output:

dafny
method findMax(arr: array<int>) returns (maxVal: int)
    requires arr.Length > 0
    ensures forall k :: 0 <= k < arr.Length ==> maxVal >= arr[k]
    ensures exists k :: 0 <= k < arr.Length && maxVal == arr[k]
{
    maxVal := arr[0];
    var i := 1;
    while i < arr.Length
        invariant 1 <= i <= arr.Length
        invariant forall k :: 0 <= k < i ==> maxVal >= arr[k]
        invariant exists k :: 0 <= k < i && maxVal == arr[k]
    {
        if arr[i] > maxVal {
            maxVal := arr[i];
        }
        i := i + 1;
    }
}
Example 3: Class with Methods

Python Input:

python
class BankAccount:
    def __init__(self, balance):
        self.balance = balance

    def deposit(self, amount):
        self.balance += amount

    def withdraw(self, amount):
        if amount <= self.balance:
            self.balance -= amount
            return True
        return False

Dafny Output:

dafny
class BankAccount {
    var balance: int

    constructor(balance: int)
        requires balance >= 0
        ensures this.balance == balance
    {
        this.balance := balance;
    }

    method deposit(amount: int)
        requires amount >= 0
        modifies this
        ensures balance == old(balance) + amount
    {
        balance := balance + amount;
    }

    method withdraw(amount: int) returns (success: bool)
        requires amount >= 0
        modifies this
        ensures success ==> balance == old(balance) - amount
        ensures !success ==> balance == old(balance)
        ensures success <==> amount <= old(balance)
    {
        if amount <= balance {
            balance := balance - amount;
            return true;
        }
        return false;
    }
}

Python Input:

python
def binary_search(arr, target):
    left, right = 0, len(arr) - 1
    while left <= right:
        mid = (left + right) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

Dafny Output:

dafny
method binarySearch(arr: array<int>, target: int) returns (index: int)
    requires forall i, j :: 0 <= i < j < arr.Length ==> arr[i] <= arr[j]
    ensures 0 <= index < arr.Length ==> arr[index] == target
    ensures index == -1 ==> forall k :: 0 <= k < arr.Length ==> arr[k] != target
{
    var left := 0;
    var right := arr.Length - 1;

    while left <= right
        invariant 0 <= left <= arr.Length
        invariant -1 <= right < arr.Length
        invariant forall k :: 0 <= k < left ==> arr[k] < target
        invariant forall k :: right < k < arr.Length ==> arr[k] > target
    {
        var mid := (left + right) / 2;
        if arr[mid] == target {
            return mid;
        } else if arr[mid] < target {
            left := mid + 1;
        } else {
            right := mid - 1;
        }
    }
    return -1;
}

Best Practices

  1. Start with specifications: Think about preconditions and postconditions first
  2. Use appropriate types: Choose nat for non-negative values, seq for immutable lists
  3. Add loop invariants: Essential for verification, document loop behavior
  4. Prefer functions over methods: Functions are easier to verify and use in specs
  5. Test incrementally: Verify small pieces before combining
  6. Use helper functions: Break complex logic into smaller, verifiable pieces
  7. Document assumptions: Make implicit Python assumptions explicit in Dafny
  8. Handle edge cases: Explicitly handle empty collections, zero values, etc.

Key Differences: Python vs Dafny

  1. Typing: Python is dynamically typed, Dafny is statically typed
  2. Mutability: Python has mutable lists/dicts, Dafny prefers immutable sequences
  3. Verification: Dafny requires specifications and proofs
  4. Loops: Dafny requires loop invariants for verification
  5. Exceptions: Python uses exceptions, Dafny uses preconditions
  6. None: Python has None, Dafny uses Option<T> datatype
  7. Functions vs Methods: Dafny distinguishes pure functions from methods with side effects

Limitations and Considerations

  1. Dynamic features: Python's dynamic typing and reflection are not directly translatable
  2. Libraries: Python standard library functions need manual translation
  3. Generators: Python generators require different approaches in Dafny
  4. Decorators: Python decorators don't have direct Dafny equivalents
  5. Multiple inheritance: Dafny has limited inheritance support
  6. Performance: Verification adds compile-time overhead
  7. Learning curve: Dafny specifications require understanding of formal methods

Resources

© ArabelaTso, Apache-2.0. Rendered from Markdown: HTML in the file is shown as text, images as links, and headings moved down two levels. Raw file

Files

SKILL.md and 1 other file (references) in skills/python-to-dafny-translator of ArabelaTso/Skills-4-SE.

  • SKILL.md
  • references/translation_patterns.md

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Python To Dafny Translator next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Python To Dafny Translator compared with similar skills
SkillStarsUsed inTokensAuto-checkLicenceRepo updated
Python To Dafny Translator this skillArabelaTso/Skills-4-SE253—~3.1kAutomated safety check: PassApache-2.0
China Travel Kittczyliu/china-travel-kit194—~1.3kAutomated safety check: PassMIT
Technology Searchfreestylefly/wesight943—~3.3kAutomated safety check: PassMIT
Translate Popython/python-docs-zh-tw284—~793Automated safety check: PassCustom licence
Obs Build LogsNuitka/Nuitka15k—~849Automated safety check: PassAGPL-3.0
Update Gui TranslationsArduPilot/MethodicConfigurator163—~1.5kAutomated safety check: PassGPL-3.0

Similar skills

  • China Travel Kit

    tczyliu/china-travel-kit

    Research and plan first-time independent trips in China with bilingual, source-aware city data and official live-check entry points.

    194 GitHub stars~1.3k tokensUpdated 1 mo ago
    Writing & ContentAuto-check passed

  • Technology Search

    freestylefly/wesight

    Search tech blogs, developer forums, and IT media (TechCrunch, Hacker News, 36氪, etc.) for software and hardware industry updates with heat ranking and EN↔CN translation.

    943 GitHub stars~3.3k tokensUpdated 6 days ago
    Writing & ContentAuto-check passed

  • Translate Po

    python/python-docs-zh-tw

    Official

    Translates PO file entries from English to Traditional Chinese (zhTW) following project conventions.

    284 GitHub stars~793 tokensUpdated 2 days ago
    Writing & ContentAuto-check passed

  • Obs Build Logs

    Nuitka/Nuitka

    Access and diagnose openSUSE Build Service (OBS) package build logs.

    15k GitHub stars~849 tokensUpdated yesterday
    Writing & ContentAuto-check passed

  • Update Gui Translations

    ArduPilot/MethodicConfigurator

    Update existing GUI translations using AI assistance. An agent skill from ArduPilot/MethodicConfigurator.

    163 GitHub stars~1.5k tokensUpdated yesterday
    Writing & ContentAuto-check passed

  • Check Terminology

    python/python-docs-zh-tw

    Official

    Checks terminology consistency against project glossary and identifies zhCN terms that need conversion to zhTW.

    284 GitHub stars~705 tokensUpdated 2 days ago
    Writing & ContentAuto-check passed

More from ArabelaTso/Skills-4-SE

All 151 skills in this repo

  • Framework Migration Assistant

    ArabelaTso/Skills-4-SE

    Automatically migrate Python web applications between frameworks (Flask → FastAPI, Django → FastAPI).

    253 GitHub stars~1.9k tokensUpdated 1 mo ago
    Auto-check passed

  • Metamorphic Test Generator

    ArabelaTso/Skills-4-SE

    Generate test cases using metamorphic testing by applying transformations based on metamorphic properties.

    253 GitHub stars~798 tokensUpdated 1 mo ago
    Auto-check passed

  • Reproduction Trace Instrumenter

    ArabelaTso/Skills-4-SE

    Instruments programs to capture execution traces specifically for reproducing reported bugs, enabling consistent replay and diagnosis of failures.

    253 GitHub stars~2.4k tokensUpdated 1 mo ago
    Auto-check passed

  • Spring Mvc To Boot Migrator

    ArabelaTso/Skills-4-SE

    Automatically migrate Spring MVC applications to Spring Boot.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

  • State Snapshot Instrumenter

    ArabelaTso/Skills-4-SE

    Instrument programs (Python, C/C++, Java) to capture snapshots of key program states at runtime, including variables, memory, and call stacks.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

Works with

Categories

Questions about Python To Dafny Translator

What does Python To Dafny Translator do?

Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable. Python To Dafny Translator is an agent skill from ArabelaTso/Skills-4-SE. Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring the generated code is well-typed, executable, and verifiable.

When should I use Python To Dafny Translator?

Python To Dafny Translator fits situations like: the user asks to convert Python code to Dafny; port Python programs to Dafny; add formal verification to Python code; create Dafny versions of Python algorithms with specifications.

How do I install Python To Dafny Translator in Claude Code?

Run `npx skills add ArabelaTso/Skills-4-SE --skill python-to-dafny-translator -a claude-code`. Or copy the skill folder (skills/python-to-dafny-translator in ArabelaTso/Skills-4-SE) into .claude/skills/python-to-dafny-translator in your project. Claude Code loads it when a task matches its description.

How do I install Python To Dafny Translator in Codex?

Run `npx skills add ArabelaTso/Skills-4-SE --skill python-to-dafny-translator -a codex`. Or copy the skill folder (skills/python-to-dafny-translator in ArabelaTso/Skills-4-SE) into .agents/skills/python-to-dafny-translator in your project. Codex loads it when a task matches its description.

Can I use Python To Dafny Translator in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add ArabelaTso/Skills-4-SE --skill python-to-dafny-translator -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/python-to-dafny-translator, .gemini/skills/python-to-dafny-translator, .github/skills/python-to-dafny-translator and .opencode/skills/python-to-dafny-translator in your project.

What does Python To Dafny Translator need to run?

SKILL.md names no scripts, command-line tools or credentials: Python To Dafny Translator is instructions for the agent only. Our summary lists: Python 3.

Does Python To Dafny Translator access the network?

SKILL.md names 1 domain. As links in the text: dafny.org. This is read from the text; nothing was executed.

Is Python To Dafny Translator safe to install?

Our automated static check of SKILL.md found no risky patterns, such as piping downloads into a shell, reading credential files or hidden Unicode. It is not a guarantee. Review the folder before installing.

What licence does Python To Dafny Translator use?

Python To Dafny Translator is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Python To Dafny Translator use?

About 3.1k tokens (SKILL.md is roughly 13k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full. Its references folder adds about 2.7k tokens, read only when the agent opens those files.

What are the alternatives to Python To Dafny Translator?

Skills that share tags, products or a category with Python To Dafny Translator: China Travel Kit (tczyliu/china-travel-kit, 194 stars), Technology Search (freestylefly/wesight, 943 stars), Translate Po (python/python-docs-zh-tw, 284 stars) and Obs Build Logs (Nuitka/Nuitka, 15k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Python To Dafny Translator?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 151 skills in this directory. The repository was last updated on August 21, 2026.

Source: ArabelaTso/Skills-4-SE on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.