Spartan

pqcheck is a zero-dependency Python assurance and property-testing tool for post-quantum cryptographic implementations: KEMs, digital signatures, and wire-format codecs. Instead of known-answer tests, it checks metamorphic relations and specification invariants derived from FIPS 203/204 and the Falcon spec: FO implicit-rejection binding and liveness, encoding canonicality, declared-length wrap boundaries, guard-fill bit-exclusion, hint ordering. Every check produces a Claim with one of four verdicts and there is no PASS: NOT_REACHED is never counted as clean, and DEFECT_FOUND requires a reproducer. The problem it solves: PQC libraries are new, and new crypto code has edge cases that slip past normal tests. pqcheck hunts the wrong-length, malformed, and boundary inputs and proves each finding with a standalone reproducer, under the rule that nothing counts until it replays standalone with a control. Written from scratch during the event, October 26 to November 4.