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 · Cyprus University of Technology, Cyprus
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
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 ).
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
Process stage
S1–S2 Monitor, Select
∙
∙
∙
∙
∙
∘
∙
S3 Match
∙
∘
∘
∙
S4 Construct
∙
S5–S6 Gather, Adjudicate
∙
∙
∘
∘
∙
∙
∘
∙
∙
S7 Justify
∙
∘
∙
∙
∘
∘
∙
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⊢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
∃x.¬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
∀x∈S.P(x)
S is the perturbation set an adversary actually uses.
Wrong specification set, not unsoundness: an L∞ ball may cover only a limited subset of the manipulations that matter here (Section VII ).
Quantitative bound
Pr[φ]⋈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
τ⊨φ
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 .
≤ 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⊢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?
Eused⊨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[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 )
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.
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.
Automated fact-checking (AFC) systems retrieve evidence and predict claim veracity, yet evaluations omit simple baselines, systems are developed for a single benchmark and cannot be trusted to generalise across domains. No prior work cross-evaluates the full two-stage retrieve-then-verify pipeline across diverse datasets, complementing retrieval-only studies (Thakur et al., 2021) and single-stage benchmarking studies (Calamai et al., 2025). We benchmark nine models, ranging from random and sparse baselines to fine-tuned transformers, zero-shot LLMs, and the two highest-ranked systems from the AVeriTeC 2025 shared task, across four datasets spanning scientific, open-web, and climate domains. Three findings stand out: (1) on ClimateCheck claim-only and fine-tuned models outperform zero-shot LLM and top-performing AVeriTeC 2025 systems, highlighting that noisy evidence can degrade veracity prediction; (2) system rankings are strongly domain- and metric-dependent: the best model on SciFact (macro-F1 0.70) drops to 0.31 on ClimateCheck, while the AVeriTeC 2025 winner and runner-up swap rankings based on evaluation metrics and datasets; (3) replacing retrieved evidence with gold annotations improves veracity accuracy by 14-22 points across models, confirming retrieval remains primary bottleneck. We release code, pre-processed datasets, and all results to support reproducible AFC research.
Aida Usmanova, Zangir Iklassov, Markus Leippold +1
Leuphana University of Lüneburg · MBZUAI · University of Zurich
Fact-checking systems must be scalable and epistemically trustworthy. We introduce Althea, a retrieval-augmented system for user-driven claim evaluation that matches standard pipelines on AVeriTeC while improving supported/refuted discrimination. A longitudinal survey experiment (N=961) treats a ten-day follow-up as a fading test: after modeling a verification procedure, we remove the system and ask whether users reproduce it unaided, testing metalearning rather than one-time accuracy. We compare two AI-assisted treatments, Exploratory (guided reasoning) and Summary (synthesized verdicts), against two baselines, unrelated news and Self-search. The treatments yield the strongest immediate accuracy and confidence gains but do not survive the fading test: on unseen claims they perform no better than news, while Self-search, with no procedure to fade, retains a large advantage. This reveals a factchecking-metalearning tradeoff: conditions that most improve immediate accuracy are least likely to produce metalearning, cautioning against treating AI-delivered verdicts as a source of durable literacy gains.
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