Proof Verification
Skill id:
proof-verification
Generated from JSON Schema — do not edit by hand. Run bun run cat-harness/scripts/gen-schema-docs.ts.
Input
Input schema for the proof-verification skill. Verifies Lean proofs and tracks sorry obligations.
| Field | Type | Required | Description |
|---|---|---|---|
projectRoot | string | yes | Path to the Lean project root (containing lakefile.lean). |
targetFiles | array | no | Specific files to verify (empty = entire project). |
trackSorries | boolean | no | Whether to track and report sorry placeholders. (default: true) |
Output
Output schema for the proof-verification skill.
| Field | Type | Required | Description |
|---|---|---|---|
verified | boolean | yes | |
sorryCount | integer | yes | min: 0 |
sorries | array | no | |
errors | array | no |
sorries[]
| Field | Type | Required | Description |
|---|---|---|---|
file | string | yes | |
line | integer | yes | |
obligation | string | yes | |
reference | string | no |
errors[]
| Field | Type | Required | Description |
|---|---|---|---|
file | string | no | |
line | integer | no | |
message | string | no |