SoK: Formal Methods for Fact-Checking and Information Integrity

Nikolaos Kekatos; Theodoros Nestoridis; Charalampos Bratsas; Charalampos Dimoulas; Georgios Konstantinidis; Georgios Malogiannis; Michael Sirivianos; Andreas Veglis

cs.CLSep 19, 2026

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

Organizations: Clone Systems, Cyprus · International Hellenic University, Greece · School of Journalism and Mass Communications, Aristotle University of Thessaloniki, Greece · University of Southampton, UK ·

Abstract

An automated fact-checking system returns a label: the claim is true, or it is false. In many such systems the verdict remains the primary output. What is generally missing is a record of which document settled the question, of what would have had to be different for the verdict to change, or of whether the same claim, reworded, would have been judged the same way. We call the missing piece a warrant: a separate statement of what was guaranteed and on what grounds. Formal methods produce evidence of this kind, and regulation is beginning to ask for it, since the Digital Services Act and the AI Act both call for auditable evidence about how systems behave. Surveys of automated fact-checking are usually organised by pipeline stage, and treat logic as one technique among many. We organise the field by what is being formalised instead, which gives five levels: the claim, the reasoning, the system doing the checking, the ecosystem the claim spreads through, and the regulatory obligation. Sorting 121 works into those levels, two patterns stand out. Most of the relevant formal machinery already exists, but it was built for other domains and has rarely been applied here, and the gap is widest for verifying the checking system itself. Several stages of the routine professional fact-checkers follow also have no stated correctness criterion, and two of them, writing a claim in checkable form and correcting a verdict already published, are not formally specified in any work we coded. We close with open problems, each with a suggested first step.

Figures & tables

Panel of Figure 1 — Fig. 1: The professional fact-checking process. Automation has concentrated on ingest, triage and investigation. The four highlighted stages carry the process’s epistemic guarantees. Two of them, scoping a claim and revising a published verdict, are largely absent from automated pipelines. The other two, matching and justification, are implemented routinely but with no stated correctness criterion (Section III-C ).

Process stage
	Guo et al. [ 5 ]	Zeng et al. [ 6 ]	Kotonya & Toni [ 10 ]	Eldifrawi et al. [ 11 ]	Dmonte et al. [ 12 ]	Corsi et al. [ 13 ]	Razi et al. [ 14 ]	Qudus et al. [ 15 ]	This paper
S1–S2 Monitor, Select	$\bullet$	$\bullet$			$\bullet$	$\bullet$	$\bullet$	$\circ$	$\bullet$
S3 Match	$\bullet$	$\circ$			$\circ$				$\bullet$
S4 Construct									$\bullet$
S5–S6 Gather, Adjudicate	$\bullet$	$\bullet$	$\circ$	$\circ$	$\bullet$	$\bullet$	$\circ$	$\bullet$	$\bullet$
S7 Justify	$\bullet$	$\circ$	$\bullet$	$\bullet$	$\circ$			$\circ$	$\bullet$

TABLE I: Coverage of the main surveys of automated fact-checking and of two adjacent systematizations. Rows are the process stages of Section III , the assurance levels of Section IV , and the technique families of Section IV-A . Existing surveys concentrate on the middle of the process and on the two lowest levels; none treats the system, the ecosystem, or the regulatory obligation.

Stage	In automation	Missing criterion	Candidate formalism
S3 Match	established	semantic claim equivalence	natural logic lifted to a matching relation
S4 Construct	largely absent	faithful scoped proposition	autoformalisation; temporal and numeric calculi
S7 Justify	established	evidence entails the justification	proof-producing reasoning
S8 Correct	largely absent	principled revision under new evidence	belief revision

TABLE II: The four stages whose epistemic requirements are not formalised. S4 and S8 are largely absent from automated pipelines; S3 and S7 are implemented routinely but with no stated correctness criterion.

Assurance artefact	Guarantee form	What must hold	How it fails
Proof, derivation	$E\vdash C$	The formalisation is faithful to the claim a human wrote.	Silent mistranslation. The derivation is valid and answers a different question, so the output is a confidently wrong certificate (Section VI ).
Witness, counterexample	$\exists x.\,\neg P(x)$	The model is complete enough that a witness in the encoding is a witness in the world.	Model mismatch. The minimal unsatisfiable subset localises a conflict in the encoding rather than in the evidence.
Certificate	$\forall x\in S.\,P(x)$	$S$ is the perturbation set an adversary actually uses.	Wrong specification set, not unsoundness: an $L_{\infty}$ ball may cover only a limited subset of the manipulations that matter here (Section VII ).
Quantitative bound	$\Pr[\varphi]\bowtie p$	The model is calibrated against measured behaviour, and tractable at realistic scale.	Uncalibrated, or intractable and silently replaced by simulation (Section VIII ).
Runtime verdict	$\tau\models\varphi$	The events the property mentions are observable in the deployed system.	Incomplete instrumentation. The monitor is sound over the trace it sees and the trace omits the failure.

TABLE III: The guarantee taxonomy. The axis that matters for information integrity is not power but what the method hands to a second party. Each row states the artefact, the form of the guarantee, what must hold for it to mean anything, and how it fails in practice. The last column is the one this literature most often leaves implicit, since every row can be satisfied and still be useless.

Technique family	Artefact produced	Cost / limitation	Application in this domain	Tools	l
Proof-producing: the answer is a replayable derivation
Answer set programming	stable model + derivation	grounding blow-up	verdict from rules over KG evidence; explanation falls out of the proof	clingo, DLV	2
Description logic	entailment or clash	decidable fragments only	claim consistency against a reference ontology	HermiT, ELK	1
Horn-rule rewriting	rule chain	needs a rule base	human-readable evidence for a candidate fact	ExFaKT, AMIE	2
Interactive proof	machine-checked proof	very high human cost	metatheory of the pipeline; rarely worth it here	Coq, Isabelle	2
Witness-producing: the answer localises the conflict

TABLE IV: Formal verification techniques applicable to information integrity, grouped by the artefact each produces. l refers to the assurance stack of Section IV , and the artefact classes are those of Table III . Maturity is assessed for this domain specifically, not in general: several mature techniques have never been instantiated here.

Technique family	Indicative instance	What the second party receives
Proof-producing
Answer set programming	“ $X$ held office in $Y$ during 2019”: office-holding intervals and succession rules over the reference graph	the stable model containing the office-holding atom, plus the rule chain that derived it; the explanation is the proof, not a post-hoc rationalisation
Description logic	the claim types a municipality as the subject of a property whose domain is a person	a clash, with the minimal set of ontology axioms and asserted triples that cannot hold together
Horn-rule rewriting	a candidate fact with no direct triple in the graph	a rule chain grounded in retrievable sentences, so the reader sees which mined regularity carried the inference
Interactive proof	the operator that aggregates per-source evidence into a verdict	a machine-checked proof of a metatheorem, e.g. that adding a corroborating source can never lower a verdict
Witness-producing

TABLE V: One indicative instantiation per technique family. Each row names a concrete question in this domain, the object the method is actually given, and the artefact a second party receives. The point of the last column is that the artefact is checkable without rerunning the system: a derivation can be replayed, a witness can be inspected, a certificate can be audited against its perturbation set.

	Level	Direct	Transfer	Context	All
L1	The object	13	2	5	20
L2	The reasoning	9	21	7	37
L3	The system	4	21	13	38
L4	The ecosystem	4	12	5	21
L5	Governance	0	1	4	5
	Total	30	57	34	121

TABLE VI: The coded corpus: 121 works, each assigned to the level of its primary object and counted once, so the levels partition the corpus and the totals are exact. Every figure here is generated from the coding file by script, not maintained by hand. The bibliography carries 150 entries; the difference is works cited only outside Section V –Section IX , which are not coded.

		Proof	Witness	Cert.	Quant.	Runtime
L1	The object	8 /2	5 /0	—	—	—
L2	The reasoning	9 /14	0 /3	—	0 /4	—
L3	The system	0 /1	2 /0	1 /11	1 /4	0 /5
L4	The ecosystem	0 /7	1 /2	—	2 /3	1 /0
L5	Governance	—	—	—	—	0 /1

TABLE VII: The assurance landscape: what is formalised (rows) against the artefact the method produces (columns). Each cell reads direct /transfer over the 121 coded works, and — marks a pairing absent from the corpus. Shading tracks the transfer count, so a dark cell with a small bold number is the adoption gap in one glance. Context items yield no artefact and do not appear, and every other work appears exactly once, so the entries sum to the totals of Table VI .

		$\leq$ 2015	2016–20	2021–23	2024–26	All
L1	The object	3	5	4	8	20
L2	The reasoning	9	7	9	12	37
L3	The system	1	8	4	22	38
L4	The ecosystem	4	4	6	7	21
L5	Governance	0	0	1	4	5
	Total	17	24	24	53	121

TABLE VIII: When the corpus was written. Three undated living standards (the IFCN code, the C2PA specification, ClaimReview ) carry no publication year; they are omitted from the period columns and retained in the totals. The concentration in 2024–26 is sharpest at L3, which is the quantitative basis for the claim that the field’s centre of gravity has moved recently.

	What this level asks	Artefact that answers it	Available today?
L1 object	Which proposition is asserted? “Fell by 10%” of what population, over which interval, on which measure, against which data revision?	A typed claim with scope fixed: Cyprus registered labour force, 2025-01-01 to 2025-12-31, seasonally adjusted rate, Eurostat vintage.	No. This is stage S4, which we found has no formalised operation at all (Section III-C ); the nearest work fixes quantification for graph claims [ 48 ] .
L2 reasoning	Does the evidence entail the claim under that scope?	A derivation $E\vdash C$ : two series values, one relative-change computation, replayable by an independent checker.	Yes. Arithmetic claims of this shape are exactly where solver grounding works [ 81 ] .
L3 system	Is the checker that produced the verdict itself trustworthy?	$E_{\text{used}}\models J$ for the published justification; a robustness certificate over paraphrases of the claim; a provenance manifest for any chart image.	Partly. Provenance is standardised [ 109 ] and justification entailment is decidable here, but we identified no general mechanism that checks it (Section VII ).
L4 ecosystem	If the correction is published, does it change what people believe?	$\Pr[\text{cascade}>N]<p$ given prebunking reach $x\%$ : a PCTL property over a calibrated diffusion model.	No. Diffusion is formally modelled and classified [ 132 , 133 ] ; intervention guarantees are not stated as properties (Section VIII ).
L5 governance	Which audit obligation does this evidence discharge?	The bundle above, addressed to a named DSA risk-assessment duty.	No. The obligation is not written in a specification language (Section IX ).

TABLE IX: One claim carried through the stack: “Unemployment fell by 10% in Cyprus during 2025.” Each row gives the question its level asks, the artefact that would answer it, and whether the corpus contains a method producing that artefact today. The warrant is the tuple of artefacts in the third column, and the two rows a reader would most want are the two the literature does not supply.

Observation in the corpus	Gap	Problem
S4 has no formalised operation (Section III-C )	spec	1
Autoformalisation faithfulness unstudied here (Section VI )	spec	2
L3 certificates declare unsuitable perturbation sets	spec	3
No completeness property for evidence sets	cov	4
Decomposition has no preservation criterion	comp	5
Certificates attach to components, not pipelines	comp	6

TABLE X: Provenance of the research agenda. Each open problem of Section XI is a deduction from a specific observation in the coded corpus, not a free-standing suggestion. The middle column names the gap type: spec ification, cov erage, ad option, ev aluation or comp osition.

Automated Fact-Checking

Automated fact-checking detects checkable claims, retrieves evidence, and assesses whether that evidence supports or refutes them.

See all 139 papers

The Warrant Gap: Claim-Conditioned Re-scoring for Fact-Checking
Jun 23, 2026Arka Ujjal Dey, John CollomosseFactual Consistency Evaluation Citation Verification
How Robust Are Automated Fact-Checking Systems? A Cross-Benchmark Evaluation
Aug 26, 2026Aida Usmanova, Zangir Iklassov, Markus Leippold +1Automated Fact-Checking Scientific Claim Verification
Leuphana University of Lüneburg · MBZUAI · University of Zurich
Althea: The Fact-Checking--Metalearning Tradeoff in AI-Assisted Verification
Dec 29, 2025Svetlana Churina, Kokil Jaidka, Anab Maulana Barik +5Human-in-the-Loop Evaluation Automated Fact-Checking
Centre for Trusted Internet & Community (CTIC), National University of Singapore (NUS), Singapore · Department of Communications and New Media, Centre for Trusted Internet & Community (CTIC), National University of Singapore (NUS), Singapore · School of Computing, Centre for Trusted Internet & Community (CTIC), National University of Singapore (NUS), Singapore

Jun 23, 2026J/K move · Enter open · S save

The Warrant Gap: Claim-Conditioned Re-scoring for Fact-Checking

Arka Ujjal Dey, John Collomosse

Factual Consistency Evaluation Citation Verification Automated Fact-Checking

Open paper AskPDF arXiv

Fact-checking systems built on LLMs achieve high verdict accuracy on standard benchmarks, yet routinely output Supports labels whose cited evidence does not license the claim. Structured decomposition is the natural way to inspect those warrants, but rigid extraction protocols strip the full-claim context that facets need. We introduce SIFT -- claim-conditioned re-scoring of extracted evidence spans against the full claim -- paired with WSP (Warranted Supports Proportion), an automatic NLI check that the cited warrant entails the claim. We evaluate on FEVER, SciFact, 5PILS, and DP across four open-source backbones. SIFT recovers accuracy on cells where naive decomposition costs up to 27.6 points, while raising WSP above direct prompting; WSP itself calibrates against human gold evidence at AUC 0.92 and precision 0.98.

Abstract

Automated Fact-Checking

Explore similar work

The Warrant Gap: Claim-Conditioned Re-scoring for Fact-Checking

How Robust Are Automated Fact-Checking Systems? A Cross-Benchmark Evaluation

Althea: The Fact-Checking--Metalearning Tradeoff in AI-Assisted Verification