proof-carrying-code-generator
Generate executable code together with formal proofs certifying safety and correctness properties in Isabelle/HOL or Coq. Use when building verified software, safety-critical systems, or when formal guarantees are required. Produces code with accompanying proofs for memory safety, bounds checking, functional correctness, invariant preservation, and termination. Supports extraction to OCaml/Haskell/SML and integration with existing codebases.
93
92%
Does it follow best practices?
Impact
92%
1.01xAverage score across 3 eval scenarios
Passed
No known issues
Quality
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 (formal proofs, code generation, extraction), provides explicit trigger conditions ('Use when building verified software, safety-critical systems'), and uses domain-appropriate terminology that users in this space would naturally use. The description is well-structured, uses third person voice correctly, and occupies a distinct niche that won't conflict with other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Generate executable code together with formal proofs', 'proofs for memory safety, bounds checking, functional correctness, invariant preservation, and termination', 'extraction to OCaml/Haskell/SML', and 'integration with existing codebases'. | 3 / 3 |
Completeness | Clearly answers both what ('Generate executable code together with formal proofs certifying safety and correctness properties') AND when ('Use when building verified software, safety-critical systems, or when formal guarantees are required') with explicit trigger guidance. | 3 / 3 |
Trigger Term Quality | Includes strong natural keywords users would say: 'Isabelle/HOL', 'Coq', 'formal proofs', 'verified software', 'safety-critical systems', 'formal guarantees', 'memory safety', 'bounds checking', 'functional correctness', 'OCaml/Haskell/SML'. These cover both domain-specific terms and common variations. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting formal verification with specific proof assistants (Isabelle/HOL, Coq). The combination of formal proofs, specific theorem provers, and extraction targets makes it unlikely to conflict with general coding or documentation skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
85%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 skill document with excellent actionability through complete, executable Isabelle and Coq examples. The workflow is clearly structured with explicit steps and a verification checklist. Minor verbosity in the overview section and some explanatory content that Claude wouldn't need slightly reduces token efficiency.
Suggestions
Remove or significantly condense the Overview section - Claude already knows what proof-carrying code is and doesn't need the numbered list of what the skill generates
The 'Core Approaches' section could be more concise by removing the 'Steps' lists since the examples already demonstrate the workflow clearly
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The skill is reasonably efficient but includes some unnecessary explanatory content like the overview section explaining what PCC is, which Claude would already know. The workflow diagram and some introductory text could be trimmed. | 2 / 3 |
Actionability | Provides fully executable Isabelle and Coq code examples throughout, with complete proof structures, theorem statements, and extraction commands. Examples are copy-paste ready and cover multiple approaches. | 3 / 3 |
Workflow Clarity | Clear multi-step workflows with explicit sequences (specification → implementation → proof → extraction). Includes a verification checklist with explicit validation steps and the workflow diagram clearly shows the process flow. | 3 / 3 |
Progressive Disclosure | Well-structured with clear overview, detailed examples inline, and appropriate references to separate files (isabelle_pcc.md, coq_pcc.md, safety_properties.md) for framework-specific and detailed content. References are one level deep and clearly signaled. | 3 / 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.
- Repository
- ArabelaTso/Skills-4-SE
- Commit
0f00a4f
- 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.