python-to-dafny-translator
Translates Python functions into Dafny, adding types, pre/postconditions, and loop invariants sufficient for Dafny to verify. Use when formally verifying a Python algorithm, when the user wants machine-checked correctness for a critical function, or when building a verified reference implementation.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill python-to-dafny-translator97
Quality
96%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly articulates specific capabilities (Python-to-Dafny translation with verification annotations), uses appropriate domain terminology that users would naturally employ, and provides explicit trigger conditions. The description is concise yet comprehensive, covering a well-defined niche with minimal conflict risk.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Translates Python functions into Dafny', 'adding types, pre/postconditions, and loop invariants', and 'sufficient for Dafny to verify'. These are precise, technical actions. | 3 / 3 |
Completeness | Clearly answers both what ('Translates Python functions into Dafny, adding types, pre/postconditions, and loop invariants') AND when ('Use when formally verifying a Python algorithm, when the user wants machine-checked correctness for a critical function, or when building a verified reference implementation'). | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'Python', 'Dafny', 'formally verifying', 'machine-checked correctness', 'verified reference implementation', 'pre/postconditions', 'loop invariants'. Good coverage of domain-specific terms. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche combining Python-to-Dafny translation with formal verification. The specific language pair (Python→Dafny) and verification focus make conflicts with other skills very unlikely. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
92%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
Excellent skill that efficiently maps Python constructs to Dafny equivalents with concrete, executable examples. The impedance mismatch framing is clever and actionable. Minor weakness is the dangling reference to 'invariant-inference' and the monolithic structure, though the content density justifies keeping it together.
Suggestions
Clarify the 'invariant-inference' reference—either link to an actual file or inline the technique
Consider splitting the translation tables into a separate REFERENCE.md if this skill grows
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | Every section earns its place—tables compress translation rules efficiently, no explanation of what Dafny or Python are, assumes Claude knows both languages. The impedance mismatch table is dense with actionable mappings. | 3 / 3 |
Actionability | Provides executable Dafny code with complete worked example that verifies. Translation tables give concrete patterns, not vague descriptions. The output format template is copy-paste ready. | 3 / 3 |
Workflow Clarity | Clear 3-step process (extract spec → translate body → add invariants) with explicit guidance on what to do when stuck. The 'Do not' section provides validation checkpoints against common failure modes. | 3 / 3 |
Progressive Disclosure | Content is well-organized with clear sections, but references 'invariant-inference' without explaining what it is or where to find it. All content is inline rather than split, though the skill length may justify this. | 2 / 3 |
Total | 11 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
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.