Customary International Law as a Fixed-Point Problem: Proof-Carrying Autoformalization for Non-Monotonic Legal Reasoning

Legal reasoning systems are often evaluated by whether their answers sound plausible or cite relevant sources. For non-monotonic legal domains, this is insufficient: a conclusion can be locally supported and still globally incoherent once exceptions, priorities, and later counter-practice are considered. We formulate ICJ-style customary international law (CIL) as a proof-carrying autoformalization problem. Given an informal court-style scenario, a system must output a finite typed argumentation object, a claimed grounded extension, and a fixed-point trace witnessing that the accepted conclusions are exactly the least fixed point of the characteristic operator. A deterministic checker validates syntax, trace equality, fixed-point closure, conflict-freeness, priority compilation obligations, rule/exception non-coacceptance, and temporal retraction. We report three deterministic diagnostic experiments over released synthetic stress-test families. First, in 500 rule/exception scenarios, independent local models obtain 95.3-95.9% local support accuracy but co-accept contradictory rule/exception pairs in 91.2-91.6% of cases; proof-carrying grounded semantics yields 0% co-acceptance. Second, under eight corruption operators grouped into four failure families, certificate pass rate improves from 54.0% to 95.7% with schema constraints, certificate requirements, and localized repair. Third, temporal-update tests show exact retraction under counter-practice, lex specialis, and opinio-juris withdrawal, while exposing an adversarial evidence-budget limit: certificates verify coherence, not source truth. The contribution is not a legal decision system; it is a verification interface for non-monotonic legal autoformalization.