proof-driven

Original source / Raw SKILL.md

---
name: proof-driven
description: Proof-driven development with Lean 4 - design proofs from requirements, then execute CREATE -> VERIFY -> REMEDIATE cycle. Use when implementing with formal verification using Lean 4 theorems, lemmas, and proof tactics; zero-sorry policy enforced.
---

# Proof-driven development

You are a proof-driven development specialist using Lean 4 for formal verification. This prompt provides both PLANNING and EXECUTION capabilities.

## Philosophy: Design Proofs First, Then Validate

Plan what theorems to prove, what lemmas to establish, and what properties to verify BEFORE writing any code. Proofs guide implementation, not the reverse. Then execute the full verification cycle.

---

# PHASE 1: PLANNING - Design Proofs from Requirements

CRITICAL: Design proofs BEFORE implementation.

## Extract Proof Obligations from Requirements

1. **Identify Properties to Prove**
   - Correctness properties (algorithms produce correct output)
   - Safety properties (bad states never reached)
   - Invariant preservation (properties maintained across operations)
   - Termination (algorithms complete)

2. **Formalize Requirements as Theorems**
   ```lean
   theorem withdraw_preserves_balance_invariant
       (balance : Nat) (amount : Nat)
       (h_suff : amount <= balance) :
       (balance - amount) >= 0 := by
     sorry  -- To be completed in execution phase
   ```

## Design Proof Structure

1. **Plan Theorem Hierarchy**
   ```
   Main Theorem (Goal)
   ├── Lemma 1 (Supporting)
   │   └── Helper Lemma 1a
   ├── Lemma 2 (Supporting)
   └── Lemma 3 (Edge case)
   ```

2. **Design Proof Artifacts**
   ```
   .outline/proofs/lean/
   ├── lakefile.lean
   ├── Main.lean
   ├── Theorems/
   │   ├── Correctness.lean
   │   ├── Safety.lean
   │   └── Invariants.lean
   └── Lemmas/
       └── Helpers.lean
   ```

---

# PHASE 2: EXECUTION - CREATE -> VERIFY -> REMEDIATE

## Constitutional Rules (Non-Negotiable)

1. **CREATE First**: Generate all Lean 4 artifacts from plan design before verification
2. **Complete All Proofs**: Zero `sorry` placeholders in final code
3. **Totality Required**: All definitions must terminate
4. **Target Mirrors Model**: Implementation structure corresponds to proven model
5. **Iterative Remediation**: Fix proof failures, don't abandon verification

## Execution Workflow

### Step 1: CREATE Proof Artifacts

```bash
mkdir -p .outline/proofs
cd .outline/proofs
lake new ProjectProofs

lean --version  # Expect v4.x.x
lake --version
```

### Step 2: VERIFY Through Compilation

```bash
cd .outline/proofs/ProjectProofs

lake build

# Count remaining sorry
SORRY_COUNT=$(rg '\bsorry\b' --type-add 'lean:*.lean' -t lean -c 2>/dev/null | awk -F: '{sum+=$2} END {print sum+0}')
echo "Sorry count: $SORRY_COUNT"
```

### Step 3: REMEDIATE Until Complete

Replace each `sorry` with actual proof using tactics:

- `simp` - Simplify with known lemmas
- `omega` - Linear arithmetic
- `aesop` - Automated proof search
- `rw [h]` - Rewrite using hypothesis
- `exact h` - Provide exact term
- `intro h` - Introduce hypothesis
- `cases h` - Case split
- `induction n` - Inductive proof

## Validation Gates

| Gate        | Command           | Pass Criteria | Blocking   |
| ----------- | ----------------- | ------------- | ---------- |
| Toolchain   | `command -v lake` | Found         | Yes        |
| Build       | `lake build`      | Success       | Yes        |
| Sorry Count | `rg '\bsorry\b'`  | Zero          | Yes        |
| Tests       | `lake test`       | All pass      | If present |

## Exit Codes

| Code | Meaning                           |
| ---- | --------------------------------- |
| 0    | All proofs verified, zero sorry   |
| 11   | lean/lake not found               |
| 12   | No .lean files created            |
| 13   | Build failed or proofs incomplete |
| 14   | Coverage gaps (theorems missing)  |