proof-failure-explainer

Analyze and explain why Isabelle or Coq proofs fail, identifying the root cause such as type mismatches, missing assumptions, incorrect goals, unification failures, or inapplicable tactics. Use when the user encounters proof failures, error messages in formal verification, stuck proof states, or asks why their Isabelle/Coq proof doesn't work.

1.01x

Quality

92%

Does it follow best practices?

Impact

88%

1.01x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Evaluation results

86%

Coq Proof Failure Analysis Report

Type error and unification failure diagnosis

Criteria

Without context

With context

Proof 1 category

100%

Proof 2 category

50%

100%

Proof 3 category

100%

Type mismatch explanation

100%

Unification term comparison

100%

'Fails because' phrasing

Expected vs actual mismatch

100%

Corrected code examples

100%

Fix explanation

100%

reflexivity limitation

100%

Existential instantiation fix

100%

Debugging tool recommendation

Alternative approach

100%

83%

-3%

Isabelle/Coq Proof Debugging Consultation

Tactic failure and induction problem diagnosis

Criteria

Without context

With context

Tactic failure category

100%

Induction failure category

100%

Conjunction vs disjunction distinction

100%

Correct tactic for disjunction

100%

Wrong induction variable explanation

100%

IH weakness explanation

87%

75%

'Fails because' phrasing

37%

75%

Tactic goal structure mismatch

100%

Working corrected proofs

100%

Fix explanation

100%

Isabelle debugging tool

Induction diagnostic question

100%

37%

96%

Formal Verification Study Group: Proof Review

Missing assumption and incorrect goal diagnosis

Criteria

Without context

With context

Proof 1 category

100%

Proof 2 category

55%

Proof 3 category

100%

Proof 4 category

100%

Proof 5 category

100%

Counterexample for Proof 3

100%

Counterexample for Proof 4 or 5

100%

Missing precondition for Proof 2

100%

Correct tactic for Proof 1

100%

'Fails because' phrasing

85%

100%

Goal correctness verification

100%

Fixed goal for incorrect statements

100%

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

Evaluated: 29 days ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Coq Proof Failure Analysis Report Isabelle/Coq Proof Debugging Consultation Formal Verification Study Group: Proof Review

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.