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.

1.25x

Quality

83%

Does it follow best practices?

Impact

100%

1.25x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Quality

Content

67%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.

The content is highly actionable with concrete Isabelle/Coq proofs and a well-sequenced workflow, but it spends tokens re-teaching Hoare-logic fundamentals Claude already knows and inlines heavy worked examples. References are well-signaled and one level deep.

Suggestions

Trim the re-explanation of basic Hoare rules (assignment/sequence/conditional/while axioms) and the 'Correctness Types' definitions of partial vs total correctness — Claude already knows these; keep only skill-specific guidance.

Move one of the two full dual-system proofs (Isabelle+Coq) into references/verification_patterns.md and keep a single concise worked example inline to reduce token weight while preserving actionability.

Make the invariant-validation feedback loop explicit inside the workflow (e.g., 'If preservation fails, generalize the invariant and re-check initialization/preservation/postcondition') rather than leaving it as a trailing tip.

Dimension	Reasoning	Score
Conciseness	The body re-explains basic Hoare rules (assignment axiom, sequence, conditional, while) and redefines partial vs total correctness — concepts Claude already knows — and inlines two full Isabelle+Coq proofs, so it is mostly efficient but carries noticeable padding.	3 / 5
Actionability	Provides real, near-complete Isabelle and Coq proof scripts plus loop-invariant and VC-generation templates covering common cases, but proofs are explicitly marked 'abbreviated', leaving minor gaps for copy-paste use.	4 / 5
Workflow Clarity	A clear five-step workflow (analyze → invariant → VCs → proof → termination) with the 'Test invariant: Check initialization, preservation, and postcondition' checkpoint, though the fix-and-retry feedback loop is only implied rather than stated inline.	4 / 5
Progressive Disclosure	Two real one-level-deep references (hoare_logic.md, verification_patterns.md) are clearly signaled with descriptions and 'Load these references when' guidance, but the body still inlines substantial full-proof examples that could partly live in references.	4 / 5
	Total	15 / 20 Passed

Description

100%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, third-person description that concretely states capabilities, gives an explicit multi-part 'Use when' trigger, and covers its niche with synonyms for both target systems and correctness types. It is comprehensive without being vague.

Dimension	Reasoning	Score
Specificity	Lists multiple concrete actions — 'Prove program correctness using Hoare logic', 'Generate verification conditions from pre/postconditions', 'Construct loop invariants and termination arguments', 'Verify imperative programs with assignments, conditionals, and loops' — giving comprehensive coverage.	5 / 5
Completeness	Explicitly answers both 'what' ('Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications') and 'when' with a concrete 'Use when users need to: (1)-(4)' trigger list.	5 / 5
Trigger Term Quality	Comprehensive natural domain terms with synonyms: 'Isabelle or Coq' / 'Isabelle/HOL and Coq', 'partial or total correctness', 'Hoare logic', 'loop invariants', 'verification conditions', 'pre/postconditions' — exactly what a user needing formal verification would say.	5 / 5
Distinctiveness Conflict Risk	Clear niche — formal correctness proofs in Isabelle/Coq via Hoare logic — with distinct triggers and minimal overlap risk against other skills.	5 / 5
	Total	20 / 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/program-correctness-prover/SKILL.md
Commit: 4f38503

Reviewed: 19 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.