SoK: Formal Methods for Fact-Checking and Information Integrity

Authors: Nikolaos Kekatos, Theodoros Nestoridis, Charalampos Bratsas, Charalampos Dimoulas, Georgios Konstantinidis, Georgios Malogiannis, Michael Sirivianos, Andreas Veglis Venue: arXiv cs.CY, 2026 — arxiv:2609.23239

TL;DR

This systemization of knowledge surveys formal methods (logic, model checking, theorem proving, symbolic reasoning) applied to fact-checking systems. The authors organize 121 works by assurance level and identify two critical gaps: constructing checkable claims and correcting errors in published verdicts. They propose that fact-checking systems require "warranties"—explicit statements of what conditions guarantee correctness—and frame this as the missing piece between automated checking and human-validated output.

Contributions

1. Five-level assurance stack organizing formal methods by their object of formalization: claims themselves, reasoning over claims, the checking system, the broader ecosystem, and regulatory obligations.

2. Grounded account of professional fact-checking pipelines that reveals a structural gap: formal methods apply to individual stages (claim detection, evidence retrieval, verdict prediction) but rarely to end-to-end verification, and verdicts lack explicit, checkable warranties of correctness.

3. Systematic survey of 121 works categorized by pipeline stage, assurance level, and formal-method technique family.

4. Eleven concrete open problems in formalizing different aspects of fact-checking, from claim representation to multi-agent belief dynamics.

Method

The authors surveyed formal-verification and formal-reasoning literature—including logic, symbolic model checking, SAT/SMT solving, proof-producing methods, and neuro-symbolic approaches—and systematically coded each work against a two-dimensional matrix: - Pipeline stage: monitor, select, match, construct, gather, adjudicate, justify, correct, intervene - Assurance level: object (claim structure), reasoning (verdict derivation), system (the checker itself), ecosystem (how information spreads), governance (compliance/audit)

They organized 121 works by these axes, identified technique families and their guarantees (e.g., proof-producing methods return a derivation; SMT solvers return a model or a core; witness-producing methods locate minimal conflicts), and mapped which combinations are mature and which are missing.

Results

Mature combinations (proof-producing + reasoning level; symbolic model checking + system level; witness-producing at object level).

Critical gaps: - S4 (Construct): No formal framework for translating natural-language claims into machine-checkable form. Semantic normalization, quantifier handling, temporal scope, and scope ambiguity remain unresolved. - S8 (Correct): Verdicts are rarely revisable with formal guarantees. When errors surface (e.g., evidence later contradicts the published verdict), no framework exists for formally updating the justification and restating what still holds.

Key missing pieces: - End-to-end pipeline verification (almost all work is on single stages) - Runtime, probabilistic, and qualitative model checking for deployed systems - Formal treatment of how misinformation spreads among agents and how interventions work - Regulatory compliance formalism (L5)

Connections

• Related to Rumor detection on social media and Misinformation Propagation via cascade and diffusion models; formal approaches to modeling belief spread and intervention design.
• Methodologically connected to Claim detection and Evidence Retrieval as pipeline stages; and to Stance Detection and Veracity prediction for verdict assignment.
• Cited in relation to Fact-checking systems and Automated Fact Checking as a reference on technical guarantees and limitations.
• Complements Explanation in fact-checking by formalizing how fact-checkers justify their verdicts.

Notes

Strengths: Clear, honest systemization. The five-level assurance stack is a useful conceptual framework. The "warranty" framing is novel and addresses a real gap in the literature: most systems output a label, sometimes with an explanation, but almost never with a formally stated guarantee of when that label is correct. The eleven open problems are concrete and well-motivated.

Limitations: Focuses on symbolic and formal methods; largely excludes neural-network robustness and adversarial verification literature (which applies formal methods to neural systems but hasn't coalesced around fact-checking yet). The professional fact-checking gap (between what formal methods can guarantee and what a checker must hand to the public) is real but the paper defers solutions to future work. No user studies on whether formal warranties would actually change how fact-checkers operate or how the public trusts their output.

Follow-ups: (1) Constructing checkable claims—bridging NLP and formal semantics; (2) Revisable verdicts and belief revision in published output; (3) Formal modeling of intervention effectiveness in information cascades; (4) Standards and tooling for runtime verification of deployed checkers.