Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add ArabelaTso/Skills-4-SE --skill cpp-to-dafny-translatorgit clone --depth 1 https://github.com/ArabelaTso/Skills-4-SEWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/arabelatso/skills-4-se/cpp-to-dafny-translator)<a href="https://agentmods.dev/skills/arabelatso/skills-4-se/cpp-to-dafny-translator"><img src="https://agentmods.dev/badge/skills/arabelatso/skills-4-se/cpp-to-dafny-translator/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/arabelatso/skills-4-se/cpp-to-dafny-translator"><img src="https://agentmods.dev/badge/skills/arabelatso/skills-4-se/cpp-to-dafny-translator.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00096 | $0.03048 |
| Opus 5 | $0.00048 | $0.01524 |
| Sonnet 5 | $0.00019 | $0.00610 |
| Haiku 4.5 | $0.00010 | $0.00305 |
Grade A, and why
cpp-to-dafny-translator scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 12d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 450 lines — stays where its author put it; the contents beside it link to each section on GitHub.
C/C++ to Dafny Translator
Translate C/C++ programs into equivalent, verifiable Dafny code while preserving program semantics and ensuring memory safety.
Overview
This skill provides systematic guidance for translating C/C++ code to Dafny, handling memory management, pointer semantics, type conversions, and ensuring well-typed, verifiable output with appropriate specifications.
Translation Workflow
C/C++ Input → Analyze Structure → Map Types & Memory → Translate → Add Specifications → Verify
├─ Identify types, pointers, memory patterns
├─ Map C/C++ constructs to Dafny equivalents
├─ Handle memory safety and ownership
├─ Add preconditions, postconditions, invariants
└─ Validate executability and verification
Core Translation Principles
1. Memory Safety First
Dafny enforces memory safety. Every translation must:
- Replace raw pointers with safe references or arrays
- Make memory bounds explicit
- Ensure no null pointer dereferences
- Handle dynamic memory with sequences or arrays
2. Preserve Semantics
The translated code must maintain the same computational behavior, preserve function contracts, keep algorithmic complexity, and handle all edge cases including error conditions.
3. Enable Verification
Generated Dafny code must include specifications (preconditions, postconditions, invariants), be verifiable by Dafny's verifier, compile and execute correctly, and follow Dafny idioms.
Type Mapping Reference
Basic Types
| C/C++ Type | Dafny Type | Notes |
|---|---|---|
int, long |
int |
Unbounded integers in Dafny |
unsigned int |
nat |
Natural numbers (≥ 0) |
char |
char |
Single character |
bool |
bool |
Direct mapping |
float, double |
real |
Exact rationals in Dafny |
void |
() |
Unit type |
NULL |
Use Option or bounds checks |
No null pointers |
Composite Types
| C/C++ Type | Dafny Type | Notes |
|---|---|---|
int arr[] |
array<int> |
Fixed-size arrays |
int* ptr |
array<int> or seq<int> |
Depends on usage |
struct |
class or datatype |
Mutable vs immutable |
enum |
datatype |
Algebraic data types |
union |
datatype with variants |
Tagged unions |
What ships with it
3 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 12d ago First seen · 450 lines · 96 tokens per session scan A 7361a3a3aafe
cpp-to-dafny-translator is a skill published in the GitHub repository ArabelaTso/Skills-4-SE (252 stars, last pushed 22d ago), licensed Apache-2.0. It adds 96 tokens to every session and 3,048 once invoked, about $0.0005 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
cpp-pro
Writes, optimizes, and debugs C++ applications using modern C++20/23 features, template metaprogramming, and high-performance systems techniques. Use when building or refactoring C++ code requiring concepts, ranges, coroutines, SIMD optimization, or careful memory management — or when addressing performance…
cpp
Use when writing modern C++ (17/20/23). Covers RAII, smart-pointer ownership, move semantics, ranges, concepts, and eliminating undefined behavior with sanitizers.
unreal-thirdparty
Expert guide for integrating third-party C/C++ libraries into Unreal Engine 5.x projects and plugins. Covers static linking, dynamic linking (DLL/SO/dylib), Build.cs configuration, ModuleType.External, delay loading, runtime dependency staging, wrapping patterns, cross-platform considerations (Windows/macOS/Linux)…
llama-cpp
Guide for llama.cpp, the C/C++ LLM inference framework by ggml-org. Covers the C API (llama.h), GGUF format, quantization (Q4KM, Q80, IQ4XS), CMake builds, GPU backends (CUDA, Vulkan, Metal, ROCm), HTTP server with OpenAI-compatible API, embeddings, grammar constraints, function calling, LoRA, speculative decoding…
unreal-gas
Expert guide for Unreal Engine 5.x Gameplay Ability System (GAS) C++ development. Covers AbilitySystemComponent, GameplayAbilities, GameplayEffects, Attributes/AttributeSets, GameplayTags, GameplayCues, AbilityTasks, prediction/replication, and common patterns. Use when the user asks about GAS, gameplay abilities…
plooc-integration
Use when integrating, refactoring, or debugging PLOOC object-oriented C - defclass encapsulation, privatemember protection, vtable dispatch, or inheritance-style structs.