program-correctness-prover
Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications. Use when users need to: (1) Prove program correctness using Hoare logic, (2) Generate verification conditions from pre/postconditions, (3) Construct loop invariants and termination arguments, (4) Verify imperative programs with assignments, conditionals, and loops. Supports both partial correctness (if terminates, postcondition holds) and total correctness (terminates and postcondition holds) for both Isabelle/HOL and Coq.
Install with Tessl CLI
npx tessl i github:ArabelaTso/Skills-4-SE --skill program-correctness-prover93
Does it follow best practices?
Validation for skill structure
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 defines a specialized formal verification capability. It provides comprehensive coverage of what the skill does (proof generation, verification conditions, invariants), explicit trigger conditions via the 'Use when' clause, and domain-specific terminology that users in this field would naturally use. The description is well-structured, uses third person voice correctly, and carves out a distinct niche.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Generate Isabelle or Coq proofs', 'Prove program correctness using Hoare logic', 'Generate verification conditions', 'Construct loop invariants and termination arguments', 'Verify imperative programs with assignments, conditionals, and loops'. | 3 / 3 |
Completeness | Clearly answers both what (generate proofs, verification conditions, loop invariants) AND when with explicit 'Use when users need to:' clause followed by numbered trigger scenarios. Also clarifies scope with 'Supports both partial correctness... and total correctness'. | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural terms users would say: 'Isabelle', 'Coq', 'Hoare logic', 'verification conditions', 'pre/postconditions', 'loop invariants', 'termination arguments', 'partial correctness', 'total correctness', 'imperative programs'. These are precisely the terms someone working in formal verification would use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting formal verification with Isabelle/Coq and Hoare logic. Very unlikely to conflict with other skills due to the specialized domain terminology and specific proof assistant tools mentioned. | 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 with excellent actionability and workflow clarity. The complete Isabelle and Coq proof examples are particularly valuable, and the verification workflow is well-sequenced with clear validation steps. The main weakness is some verbosity in the overview and explanation sections that could be trimmed to improve token efficiency.
Suggestions
Remove or condense the Overview section - the 'How to Use' section already covers this information more actionably
Consider moving the detailed proof examples to a reference file and keeping only one abbreviated example inline to improve conciseness
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The skill is reasonably efficient but includes some unnecessary explanation (e.g., the Overview section restates what the skill does, and some concepts like Hoare logic rules are explained that Claude likely knows). The examples are thorough but could be more condensed. | 2 / 3 |
Actionability | Provides fully executable Isabelle and Coq code examples that are copy-paste ready. The verification workflow has concrete steps, and the examples show complete proofs with specific syntax for both proof assistants. | 3 / 3 |
Workflow Clarity | Clear 5-step verification workflow with explicit validation checkpoints (verify each VC, test invariant properties). The workflow includes feedback loops for checking invariant properties and the examples demonstrate the complete process from analysis to proof. | 3 / 3 |
Progressive Disclosure | Well-structured with clear overview, detailed examples inline, and references to external files (hoare_logic.md, verification_patterns.md) for deeper content. The 'Load these references when' section clearly signals when to access additional materials. | 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.
- 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.