c-cpp-to-lean4-translator

Translate C or C++ programs into equivalent Lean4 code, preserving program semantics and ensuring the generated code is well-typed, executable, and can run successfully. Use when the user asks to convert C/C++ code to Lean4, port C/C++ programs to Lean4, translate imperative code to functional Lean4, or create Lean4 versions of C/C++ algorithms.

1.06x

Quality

85%

Does it follow best practices?

Impact

87%

1.06x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Quality

Content

78%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 executable Lean4 examples and a clean one-level reference. It loses points on conciseness for restating C/C++ concepts Claude already knows and for some pattern redundancy across sections.

Suggestions

Trim the 'Understand semantics' and 'Note translation challenges' subsections in Step 1 — Claude already knows what program inputs/outputs and undefined behavior are; keep only Lean4-relevant notes.

De-duplicate the translation patterns that appear in both Step 3 and the Quick Reference table; consolidate or cross-reference to avoid repeating the same C→Lean4 mappings.

Make the Step 5 validation loop explicit (e.g., 'If lake build or #eval output differs, fix the translation and re-verify') to strengthen the feedback loop.

Dimension	Reasoning	Score
Conciseness	Mostly efficient with strong code examples, but the 'Understand semantics' and 'Note translation challenges' subsections explain concepts Claude already knows, and translation patterns are repeated across Step 3, the Quick Reference table, and the Examples section.	3 / 5
Actionability	Provides copy-paste-ready, complete Lean4 code across functions, control flow, structs, pointers, and I/O, plus a side-by-side C/C++→Lean4 quick reference table covering the common cases.	5 / 5
Workflow Clarity	A clear six-step sequence with validation checkpoints in Step 5 (lake build, #eval test cases, compare outputs, edge cases), but the error-recovery loop is implied rather than an explicit validate→fix→retry cycle.	4 / 5
Progressive Disclosure	SKILL.md is an overview that clearly signals one one-level-deep reference (translation_patterns.md) for the comprehensive pattern catalog, with overview-level patterns kept inline; the referenced file exists and matches the link.	5 / 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 answers both what the skill does and when to use it, with natural trigger phrases and a distinct niche. The only gap is the absence of file-extension triggers, which keeps trigger term quality just below the top anchor.

Dimension	Reasoning	Score
Specificity	Lists multiple concrete actions — translate C/C++ to Lean4, preserve program semantics, ensure well-typed, executable, and runnable code — giving comprehensive coverage of the translation capability.	5 / 5
Completeness	Explicitly states what it does (translate C/C++ to equivalent Lean4 preserving semantics) and when to use it with a concrete 'Use when...' clause listing several trigger phrases.	5 / 5
Trigger Term Quality	Covers natural synonyms users would say ('convert', 'port', 'translate', 'create Lean4 versions') but omits file-extension triggers like .c/.cpp that anchor 5 expects.	4 / 5
Distinctiveness Conflict Risk	Occupies a clear niche (C/C++ → Lean4 translation) with distinct, specific triggers and minimal overlap risk with other skills.	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/c-cpp-to-lean4-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.