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 known issues

Quality

Content

72%

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

This is a strong, actionable skill with excellent code examples and good progressive disclosure. The main weaknesses are some verbosity in introductory sections and missing explicit validation feedback loops in the workflow. The comprehensive type mappings and translation patterns provide real value for the translation task.

Suggestions

Trim the Overview and Core Translation Principles sections - Claude already understands memory safety and semantic preservation concepts

Add explicit feedback loops to the Translation Process, e.g., 'Step 4: Add Verification Annotations → Run verifier → If fails, strengthen invariants → Re-verify'

Dimension	Reasoning	Score
Conciseness	The skill contains some unnecessary explanatory text (e.g., 'This skill provides systematic guidance...', 'Dafny enforces memory safety') that Claude already knows. The type mapping tables and translation patterns are efficient, but the overview and principles sections could be tightened.	2 / 3
Actionability	Excellent executable code examples throughout with complete, copy-paste ready Dafny translations. Each pattern shows both C/C++ input and verified Dafny output with proper specifications, invariants, and ensures clauses.	3 / 3
Workflow Clarity	The 5-step translation process is clearly sequenced, but validation checkpoints are weak. Step 5 says 'Run Dafny verifier' and 'Fix verification errors' but lacks explicit feedback loops (e.g., 'If verification fails, check invariants first, then preconditions'). The verification checklist is good but comes at the end rather than integrated into the workflow.	2 / 3
Progressive Disclosure	Well-structured with clear sections progressing from overview to patterns to challenges to full examples. References to external files (type_mappings.md, memory_patterns.md, verification_guide.md) are clearly signaled and one level deep.	3 / 3
	Total	10 / 12 Passed

Description

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, includes natural trigger terms, explicitly states both what the skill does and when to use it, and occupies a highly distinctive niche. The description uses proper third-person voice and provides comprehensive coverage of the skill's scope without being verbose.

Dimension	Reasoning	Score
Specificity	Lists multiple specific concrete actions: 'Translate C/C++ programs to equivalent Dafny code', 'preserving semantics', 'ensuring verification', and explicitly mentions handling 'functions, structs, pointers, arrays, memory management' with clear output qualities (well-typed, executable, verifiable).	3 / 3
Completeness	Clearly answers both what ('Translate C/C++ programs to equivalent Dafny code while preserving semantics') AND when ('Use when users ask to convert, translate, or port C/C++ code to Dafny, or when they need to formally verify C/C++ algorithms').	3 / 3
Trigger Term Quality	Includes natural keywords users would say: 'convert', 'translate', 'port', 'C/C++', 'Dafny', 'formally verify', 'verification'. These cover common variations of how users would phrase such requests.	3 / 3
Distinctiveness Conflict Risk	Highly distinctive niche combining two specific languages (C/C++ and Dafny) with formal verification context. Very unlikely to conflict with other skills given the specialized domain of C/C++ to Dafny translation.	3 / 3
	Total	12 / 12 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 — 11 / 11 Passed

Validation for skill structure

No warnings or errors.

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Reviewed: 4 months 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.