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

92%

Does it follow best practices?

Impact

100%

1.25x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Evaluation results

100%

25%

Formal Correctness Proof: Running Product Algorithm

Loop invariant construction and partial correctness proof

Criteria

Without context

With context

Invariant initialization

100%

Invariant preservation

100%

Invariant postcondition implication

100%

Bounds in invariant

100%

Partial progress in invariant

100%

Assignment rule backward

87%

100%

Sequence rule chaining

100%

Coq Hoare triple notation

100%

Coq state-based predicates

100%

Postcondition generalization strategy

25%

100%

VC list completeness

100%

Automation tactics

100%

15%

Formal Total Correctness Proof: Euclidean GCD

Total correctness with variant function and termination argument

Criteria

Without context

With context

Partial vs total distinction

100%

Total correctness notation

100%

Variant function stated

100%

Variant non-negative

100%

Variant strictly decreasing

100%

Termination VC included

100%

Step 5 workflow

100%

Isabelle triple notation

50%

100%

Isabelle state lambda

25%

100%

Loop invariant GCD property

100%

Automation in Isabelle proof

100%

Sequence rule in loop body

16%

100%

19%

Formal Correctness Proof: Sorting Two Variables and Clamped Difference

Weakest precondition and conditional branch verification

Criteria

Without context

With context

WP backward reasoning

100%

Assignment substitution

100%

First branch condition added

100%

Second branch condition added

100%

Both branches proven separately

100%

Consequence rule identified

100%

Coq double-brace notation

100%

Coq state predicates

100%

Sequence rule intermediate

88%

100%

Automation for arithmetic

100%

Program component identification

100%

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Evaluated: 29 days 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.