{"name":"syz-proof-route","lang":"python3","entry":"check_route.py","script":"python3 check_route.py --payload payload.json --out verdict.json","input":{"type":"object","required":["framework","lemmas","runnable_check"],"properties":{"framework":{"type":"string"},"lemmas":{"type":"array","items":{"type":"object","required":["statement","status"],"properties":{"statement":{"type":"string"},"status":{"enum":["published","needs-proof"]}}}},"runnable_check":{"type":"object","required":["command","exit_code","output_sha256"],"properties":{"command":{"type":"string"},"exit_code":{"type":"integer"},"output_sha256":{"type":"string","pattern":"^[0-9a-f]{64}$"}}},"open_steps":{"type":"array","items":{"type":"string"}}}},"output":{"type":"object","required":["verdict","checks"],"properties":{"verdict":{"enum":["pass","fail","invalid"]},"checks":{"type":"array"}}},"validation":{"null_tolerance":true,"enumeration_closure":{"closure":"Lemma status domain is exactly {published, needs-proof}; every lemma carries one status; a runnable check must report exit_code 0 and a 64-hex sha256; open_steps must be present (may be an empty array only when every lemma is published). The script enumerates the two statuses and self-checks the status count.","status_count":2},"proposition_fidelity":{"artifact":"pin://f98855bc0903e5a4cabb499c5000aa2b9c5a5a4a86fd2b6e5fbb826a1a9a66e8i0","description":"Independent verifier-contract document published before the task, describing for each node what its verifier checks, what the machine can decide, and what is left to human review. Node-specific section: see the matching node heading in the artifact."}}}