cpp-to-dafny-translator

Translate C/C++ programs to equivalent Dafny code while preserving semantics and ensuring verification. Use when users ask to convert, translate, or port C/C++ code to Dafny, or when they need to formally verify C/C++ algorithms using Dafny's verification capabilities. Handles functions, structs, pointers, arrays, memory management, and ensures the generated Dafny code is well-typed, executable, verifiable, and can successfully run.

1.00x

Quality

86%

Does it follow best practices?

Impact

96%

1.00x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Quality

Content

81%Weight 40%Scale 1-5

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

A highly actionable, well-structured skill body with complete executable examples and a clear verified workflow. Its main weakness is verbosity from redundant workflow restatements and trivial examples, plus some inline content that duplicates the bundled reference files.

Suggestions

Collapse the 'Translation Workflow' diagram, 'Core Translation Principles', and 'Translation Process' into a single sequenced workflow section to remove redundancy and tighten conciseness.

Drop or condense trivial examples (add, max) that demonstrate concepts Claude already knows, keeping only the illustrative non-obvious cases like pointer arithmetic and verification annotations.

Move the full basic/composite type-mapping tables into references/type_mappings.md and keep only a short summary inline, reducing overlap with the referenced bundle file.

Dimension	Reasoning	Score
Conciseness	Mostly efficient and useful, but includes redundancy — the 'Translation Workflow' diagram, 'Core Translation Principles', and 'Translation Process' steps restate the same workflow, and trivial examples (add, max) explain concepts Claude already knows — so it could be tightened.	3 / 5
Actionability	Fully executable, copy-paste-ready Dafny code with paired C/C++ originals covering the common cases (functions, pointers/arrays, structs, control flow, memory, verification annotations); no pseudocode.	5 / 5
Workflow Clarity	Clear five-step sequence with explicit validation and a feedback loop in Step 5 ('Run Dafny verifier. Fix verification errors. Test with concrete examples'), plus a verification checklist of checkpoints; this is not a destructive/batch operation so the 3-cap does not apply.	5 / 5
Progressive Disclosure	Good structure with clearly signaled one-level-deep references to real files (type_mappings.md, memory_patterns.md, verification_guide.md), but substantial type-mapping tables and code patterns are inlined that overlap with those references, so content is not fully appropriately split.	4 / 5
	Total	17 / 20 Passed

Description

92%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

A strong, specific description that clearly states capabilities and trigger conditions with good synonym coverage. Its only gap is the absence of file-extension triggers, which keeps trigger term quality at 4 rather than 5.

Dimension	Reasoning	Score
Specificity	Lists multiple specific concrete actions with comprehensive coverage: 'Translate C/C++ programs to equivalent Dafny code', 'preserving semantics', 'ensuring verification', and explicitly enumerates 'functions, structs, pointers, arrays, memory management' plus ensures code is 'well-typed, executable, verifiable, and can successfully run'.	5 / 5
Completeness	Explicitly answers both what ('Translate C/C++ programs to equivalent Dafny code while preserving semantics and ensuring verification') and when ('Use when users ask to convert, translate, or port C/C++ code to Dafny, or when they need to formally verify') with concrete trigger phrases.	5 / 5
Trigger Term Quality	Good coverage of natural user terms including synonyms ('convert, translate, or port') and 'formally verify', but no file extensions (.c, .cpp, .dfy) are mentioned, leaving a few natural variations missing.	4 / 5
Distinctiveness Conflict Risk	Occupies a clear niche (C/C++ → Dafny formal verification) with distinct triggers; the combination of source language, target language, and verification goal makes conflict with other skills minimal.	5 / 5
	Total	19 / 20 Passed

Validation

100%

Warnings & errors only

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository: ArabelaTso/Skills-4-SE
Path: skills/cpp-to-dafny-translator/SKILL.md
Commit: 4f38503

Reviewed: 5 days ago

Table of Contents

Discovery Implementation Validation

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.