skills.rest
sunblaze-ucb
sunblaze-ucbOFFICIAL
Explore all skills by this author →
GitHub

vero-source-dafny

Translate Dafny source code into Lean 4 syntax.

2|Updated Jul 4, 2026
Search Tags:#translation#formal verification#Lean 4#programming language#Dafny
One-click install
npx skills add https://github.com/sunblaze-ucb/vero --skill vero-source-dafny
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: vero-source-dafny
Source: https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-dafny
Command: npx skills add https://github.com/sunblaze-ucb/vero --skill vero-source-dafny

SYSTEM DOCUMENTATION & REQUIREMENTS

💡 This Skill includes scripts (resource) and references (resource) components.

What problem does it solve?

This Skill translates Dafny source code to Lean 4, facilitating the use of Lean 4 in formalizing and verifying Dafny programs.

Core Features & Use Cases

  • Dafny to Lean 4 Translation: Converts Dafny source code into Lean 4 syntax for formal verification.
  • Curated Mappings: Provides Dafny-specific classification rules, type mappings, and patterns for the translation process.
  • Use Case: For a Dafny program with complex data types and functions, this Skill automates the conversion to Lean 4, enabling users to leverage Lean 4's formal verification capabilities.

Quick Start

Translate the Dafny source code in 'source.dfy' to Lean 4 using the vero-source-dafny skill.

Frequently Asked Questions about vero-source-dafny

High-intent search queries and answers about installing and using this skill.

FAQPage Schema
How do I translate Dafny source code to Lean 4 for formal verification?▼

Translating Dafny to Lean 4 requires mapping Dafny constructs to Lean 4 paradigms using curated classification rules and type mappings. This Skill automates that conversion for formal verification purposes.

What is the process for mapping Dafny constructs to Lean 4 paradigms?▼

Mapping Dafny constructs to Lean 4 paradigms involves applying curated classification rules and type mappings that translate Dafny-specific data types and functions into equivalent Lean 4 syntax for formal verification.

Do I need to know both Dafny and Lean 4 syntax to convert Dafny programs?▼

Yes, converting Dafny programs to Lean 4 requires knowledge of both Dafny and Lean 4 syntax. This prerequisite ensures you can interpret the translated output and leverage Lean 4's formal verification capabilities effectively.

Can I use this Dafny to Lean 4 translation for programs with complex data types?▼

Yes, Dafny to Lean 4 translation supports programs with complex data types and functions. It automates the conversion of these intricate structures into Lean 4 syntax, allowing you to formalize and verify Dafny programs.

Why translate Dafny programs to Lean 4 instead of verifying them directly in Dafny?▼

Translating Dafny to Lean 4 lets you leverage Lean 4's formal verification capabilities for Dafny programs. Curated mappings ensure accurate paradigm translation, providing an alternative verification pathway for complex Dafny codebases.

Are there limitations when converting Dafny source code to Lean 4 syntax?▼

Converting Dafny to Lean 4 requires knowledge of both languages' syntax and may involve limitations based on how Dafny constructs map to Lean 4 paradigms. The curated mappings focus on type and pattern translation accuracy.

Related Skills

Explore More Software Engineering Skills→
sunblaze-ucbsunblaze-ucb
2

vero-translate

Translate verified Dafny, Verus, or Coq code into Lean 4 benchmark projects.

Official
Advanced
rainoftimerainoftime
17

dafny-verifier

Write Dafny programs with formal specifications and automated proofs.

Community
Intermediate
santosomarsantosomar
1

formal-spec-generator

Routes formal specification requests to appropriate tools like TLA+ and Dafny based on input type and verification goals.

Community
Intermediate
sunblaze-ucbsunblaze-ucb
2

vero-dafny-pitfalls

Translate Dafny constructs like ghost variables and maps to Lean 4.

Official
Advanced