GPN CTF 2026 — Customer Service: Three Bugs in a holpy Proof Checker
Platform GPN CTF 2026 (kitctf) Difficulty Medium-Hard OS Misc — holpy proof checker, LCF-style higher-order logic Tags reading 115 lines of checker glue around holpy's monitor, spotting list == 1 as a dead branch, recognising Theorem.get_extension always re-axiomatizes, exploiting concl.is_const('false') as a name comparison in an EmptyTheory scope, declaring a homemade false constant and proving it with a one-line theorem rule Customer Service is the GPN CTF 2026 misc challenge that builds an LCF-style higher-order-logic proof assistant from holpy, pretends to forbid axioms, and gets its guard wrong three ways. The exploit is a three-item JSON payload: declare a false constant of our own, axiomatize it, ship a one-line proof. The flag spells the lesson: ...