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

Preview

This is a new way to view eval results. We're still working on it, so the layout may change.

Run	Type	Date	Status
baseline vs usage-spec With / without context 7 months ago Completed	With / without context	7 months ago	Completed

Eval run

019cc49c-8d2c-72cf-856e-1423d0ba2c40

Run 7 months ago

Stats are not available yet

The run is available. Its result stats will appear here when they are ready.

Repository: ArabelaTso/Skills-4-SE
Path: skills/program-correctness-prover/SKILL.md
Commit: 4f38503

Evaluated: 7 months ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Formal Correctness Proof: Running Product Algorithm Formal Total Correctness Proof: Euclidean GCD Formal Correctness Proof: Sorting Two Variables and Clamped Difference

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.