SKILL.md
Transaction Protocol Reasoning
Use this skill when a protocol is already given (paper, spec, pseudocode, implementation notes) and you need to understand what it guarantees and how its rules imply commit/abort behavior.
This skill does not ask you to invent a protocol. It teaches how to read a protocol description as a set of rules, turn those rules into checkable predicates/invariants, and then reason about safety vs conservatism.
What “done” looks like
By the end you should have:
- a one-page Protocol Ledger (state + rules + invariants)
- a minimal example pack (3–6 tiny histories) that exercises boundaries
- a clear statement of:
- the protocol’s proof object (what metadata it relies on), and
- its likely false-abort and unsafe-commit failure modes
Quick Reference (pick the next file to read)
| If you need… | Read |
|---|---|
| A step-by-step protocol reading workflow | protocol-analysis-workflow.md |
| Inventory protocol state + what each field proves | state-and-metadata-modeling.md |
| Restate read/write/validate/commit/abort as explicit rules | operation-rule-analysis.md |
| Extract invariants from rules (and distinguish conservative ones) | invariant-extraction.md |
| Build a small history suite that hits boundary behavior | example-construction.md |
| Build minimal counterexamples (unsafe commit vs conservative abort) |