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)

Raw schema · ✎ Edit

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

Raw schema · ✎ Edit