# Proof Writer Crypto

> Write and audit cryptographic protocol proofs and theorem drafts. Use when checking soundness, knowledge soundness, zero-knowledge, Fiat-Shamir security, extractor or simulator design, hidden model assumptions, reduction structure, bad-event bookkeeping, or theorem/proof overclaim.

- Skill: `5donghwan/proof-writer-crypto` (Agent Skill, multi-file: 3 files)
- Install (CLI): `npx skillmds@latest add 5donghwan/proof-writer-crypto`
- Raw SKILL.md: https://api.skillmd.com/api/skills/5donghwan/proof-writer-crypto/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: 5Donghwan (https://skillmd.com/u/5donghwan)
- Updated: 2026-09-22
- Page: https://skillmd.com/skills/5donghwan/proof-writer-crypto

---


# Proof Writer Crypto

Use this skill to turn vague cryptographic proof claims into explicit theorem
statements, explicit model assumptions, explicit proof obligations, and an
honest verdict on whether the claim is actually justified.

This skill is for cryptographic protocol proofs, not rhetorical polishing.

## Best Fit

Use this skill for:

- argument systems and proofs
- proofs or arguments of knowledge
- Sigma protocols
- Fiat-Shamir transformed protocols
- polynomial commitment sub-protocols
- NIZK, zkSNARK, and zkArgument components
- commitment-and-prove protocols
- pairing-based protocols
- recursive or composed proof systems
- appendix-grade theorem audits in papers and notes

Do not use this skill as the primary tool for:

- mechanized proofs in theorem provers
- implementation-only audits
- bare algebra with no protocol context
- intuition-only brainstorming before the theorem statement is stable

If the claim is still unstable, start in normalization mode before attempting a
full proof.

## Core Contract

Every invocation must end with exactly one classification:

- `PROVABLE AS STATED`
- `PROVABLE ONLY AFTER ADDING ASSUMPTIONS OR WEAKENING THE CLAIM`
- `NOT JUSTIFIED WITH CURRENT INFORMATION`

Never blur these categories.

If the theorem is ambiguous or under-specified, say so explicitly and stop short
of pretending the proof exists.

## Non-Negotiable Rules

### 1. Normalize before proving

Before attempting a proof, extract and restate:

- syntax
- statement or witness relation
- setup model
- security goal
- adversary model
- transcript structure
- theorem statement
- explicit assumptions

If any of these are ambiguous, list them under `AMBIGUITIES` before doing proof
work.

### 2. Separate security notions

Do not conflate:

- completeness
- soundness
- special soundness
- knowledge soundness or argument of knowledge
- honest-verifier zero-knowledge
- malicious-verifier or full zero-knowledge
- simulation soundness
- extractability
- adaptive soundness
- batch soundness

If the draft theorem mixes them, split the claim.

### 3. Never silently strengthen the model

Do not silently assume:

- ROM
- QROM
- AGM
- GGM
- CRS trapdoor access
- programmable random oracles
- algebraic adversaries
- extractable commitments
- knowledge-of-exponent style assumptions
- trusted setup properties stronger than stated

If a proof step needs one of these, mark:

- `MISSING ASSUMPTION`
- `HIDDEN MODEL RESTRICTION`

### 4. Never hide gaps with prose

Do not use words like these to cover a gap:

- clearly
- standard
- straightforward
- similarly
- routine
- by inspection
- by usual arguments

If a step is unresolved, mark it explicitly as one of:

- `UNPROVEN STEP`
- `MISSING ASSUMPTION`
- `OVERCLAIM`
- `EXTRACTOR GAP`
- `SIMULATION GAP`
- `BAD EVENT NOT BOUNDED`

### 5. The theorem must match the proof

At the end, compare the theorem statement against what the proof actually
establishes.

If the theorem claims more than the proof supports, mark `OVERCLAIM` and
propose a revised theorem.

## Use The Bundled Files

Keep context small. Read only the files relevant to the current task.

Start here:

- `templates/theorem-normalization.md`: use before proving if the theorem or
  model is not yet crisp
- `templates/soundness-audit.md`: use for soundness-only claims
- `templates/knowledge-soundness-audit.md`: use for proof-of-knowledge claims
- `templates/zero-knowledge-audit.md`: use for zero-knowledge claims
- `templates/fiat-shamir-audit.md`: use for Fiat-Shamir transformations
- `templates/hostile-reviewer.md`: use to force counterexample search

Use these checklists when relevant:

- `checklists/assumptions.md`: hidden model assumptions and theorem/proof
  alignment
- `checklists/bad-events.md`: bad-event bookkeeping
- `checklists/extractor.md`: extractor interface and overclaim checks
- `checklists/simulator.md`: simulator powers and zero-knowledge scope checks

## Required Input Shape

Whenever possible, ask for or reconstruct this structure:

```text
Protocol Name:
Security Goal:
Setup Model:
Assumptions:
Statement/Witness Relation:
Algorithms:
- Setup
- Prove
- Verify
- Extract (if claimed)
- Simulate (if claimed)

Transcript Structure:
Adversary Capabilities:
Claimed Theorem:
Relevant Prior Results / Lemmas:
Known Ambiguities:
```

If the user gives an informal draft, reconstruct this structure before
proceeding.

## Workflow

### Step 1. Gather only the local context you need

Read the theorem draft, appendix fragment, protocol description, or proof notes
that the user pointed to. Do not bulk-load unrelated files.

### Step 2. Normalize the theorem

Restate:

- quantified variables
- probability space
- security parameter
- adversary runtime class
- exact conclusion

If the theorem is still unstable, stop and return a normalization report rather
than a fake proof.

### Step 3. Build a security and model ledger

List:

- setup model
- adversary model
- oracle access
- explicit assumptions
- hidden assumptions that appear necessary
- whether the proof is standard model, ROM, QROM, AGM, or something else

### Step 4. Choose the correct audit mode

#### Soundness mode

Focus on:

- exact verifier predicate
- false-statement definition
- malformed instance handling
- challenge consistency
- random-check or batch-check loss
- final soundness bound

Do not drift into extraction unless the theorem actually claims knowledge
soundness.

#### Knowledge soundness mode

You must specify:

- extractor input
- extractor output
- oracle access
- extraction method
- whether rewinding or forking is required
- witness validation step
- extraction failure events
- runtime and success probability

Never accept a proof-of-knowledge claim unless the extraction path is explicit.

#### Zero-knowledge mode

You must specify:

- simulator input
- simulator output
- indistinguishability target
- trapdoor or programmability requirements
- abort conditions
- simulation failure probability
- honest-verifier versus full zero-knowledge scope

If the simulator needs powers not stated in the theorem, mark `SIMULATION GAP`.

#### Fiat-Shamir mode

You must check:

- exact challenge derivation
- statement binding
- transcript binding
- domain separation
- whether the public statement is hashed where required
- whether the claim is standard-model, ROM-only, or QROM-dependent
- whether a forking-style argument is actually applicable

### Step 5. Decompose the proof obligations

For nontrivial proofs, require one of:

- a game sequence
- a hybrid sequence
- a reduction
- an extractor flow
- a rewinding tree

Use this structure:

```text
[Obligation ID]
Claim:
Type: soundness / knowledge soundness / ZK / sim-soundness / binding /
  extraction / reduction step
Needed for:
Assumptions used:
Model used:
Inputs:
Output:
Proof idea:
Bad events involved:
Loss / probability degradation:
Open gap:
Status: PROVED / PARTIAL / OPEN
```

### Step 6. Maintain a bad-event ledger

Explicitly track bad events such as:

- malformed transcript acceptance
- malformed group element acceptance
- challenge collision
- domain-separation failure
- division by zero or singular extraction equations
- commitment-binding corner cases
- random linear combination failure
- rogue keys or rogue commitments
- simulator abort
- batch-verification false positives
- statement or witness ambiguity

For each bad event, record:

- definition
- where it enters
- how it is bounded
- whether it appears in the final theorem bound

### Step 7. Run the theorem/proof consistency check

Ask:

- Does the theorem claim adaptive security while the proof is only static?
- Does the theorem claim standard model while the proof uses ROM or QROM?
- Does the theorem claim knowledge soundness while the proof only shows special
  soundness?
- Does the theorem claim negligible failure without an explicit bound?
- Does the theorem claim transparency while the proof relies on trapdoor
  behavior?

If yes, mark `OVERCLAIM`.

### Step 8. Force counterexamples

Act as a hostile reviewer and enumerate the most plausible failure modes.

Prioritize:

- malformed inputs
- witness ambiguity
- extractor failure
- simulator mismatch
- Fiat-Shamir transcript non-binding
- hidden setup assumptions
- unbounded bad events
- randomized or batch checks that permit false positives

## Required Output Shape

Return sections in this order:

### A. Normalized theorem

Restate the theorem precisely.

### B. Security and model ledger

List the setup, adversary, oracle model, and assumptions actually used.

### C. Proof classification

Choose exactly one of the three required classifications.

### D. Proof skeleton or blockage report

Give the lemma structure, reduction or extractor flow, and where assumptions are
used. If the proof is blocked, say exactly why.

### E. Bad-event ledger

List bad events and whether each is bounded.

### F. Gaps or likely counterexamples

List proof gaps, theorem gaps, likely attacks, or missing assumptions.

### G. Revised theorem statement

If needed, propose a narrower defensible theorem.

## Standard Response Style

Respond in a way that is:

- crisp
- explicit
- non-handwavy
- willing to say `not justified`
- willing to weaken the theorem
- willing to stop before fake-completing an argument

Correctness matters more than pleasantness.

## Red Flags

Always detect and challenge claims like:

- "By Fiat-Shamir, security follows" with no model statement
- "By standard extraction" with no extractor
- "Zero-knowledge is immediate" with no simulator
- "The verifier checks consistency" without the exact predicate
- "This proves soundness" after showing only relation recovery
- "Transparent" despite hidden trapdoor dependence
- "Adaptive" with only static proof structure
- "Negligible" with no concrete bound source
- "Polynomial commitment binding" with no binding notion specified