An empirical look at the soundness of Git's three-way merge, motivated by the 2007 paper A Formal Investigation of Diff3. It contains:
- A minimal, reproducible counterexample in which a real
git merge(defaultortstrategy, no special config) silently produces an unsound result — a clean, conflict-free merge whose output is wrong. - A fuzzer (
fuzz.py) that searches for such merges. - A minimizer (
minimize.py) that reduces a counterexample to the smallest inputs, with a rigorous minimality argument. - The paper's own locality counterexample (a spurious conflict), reproduced in current Git.
Tested with Git 2.50.1 (Apple Git-155).
Sanjeev Khanna, Keshav Kunal, and Benjamin C. Pierce. A Formal Investigation of Diff3. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS 4855, pp. 485–496, Springer, 2007. https://www.cis.upenn.edu/~sanjeev/papers/fsttcs07_diff3.pdf DOI: 10.1007/978-3-540-77050-3_40
The paper gives the first rigorous specification of diff3: it runs a two-way
diff on (O, A) and (O, B) — never A against B directly — under the
assumption that each diff yields a maximum, non-crossing matching, then coalesces
the results into stable and unstable chunks.
Its headline results are negative. The intuition that edits to well-separated
regions never conflict is false: it fails even when the separating region is
arbitrarily long, and even when that region is textually distinct from everything
else (see examples/locality/). The one condition that does guarantee a
unique, conflict-free merge (Theorem 4.1.1) is that the separating region contain a
line that is unique in each of O, A, and B — a distinctive anchor. The
paper also shows diff3 is not idempotent, not stable, and gives no
near-success guarantee on similar replicas.
Crucially, because the paper assumes maximum matchings, all of its counterexamples are the safe kind — spurious conflicts and instability. It never exhibits a silently-wrong clean merge.
Real git merge gives up the maximum-matching assumption for speed and
readability. Its default strategy, ort, computes its internal diffs with the
histogram algorithm (even though git diff and git merge-file default to
Myers). Histogram is frequency-based, not maximal, which opens the door to a
failure the paper never had to consider: duplicating a change without raising a
conflict.
This behavior is also documented, independently, in:
Niels Glodny. Analyzing and Evaluating the Behavior of Git Diff and Merge. Bachelor's thesis, 2025. arXiv:2507.22071.
Section 4.5 ("Duplicated Changes and Missing Conflicts") describes exactly the effect reproduced here.
Files in examples/minimal/:
| File | Contents (one atom per line) | Change from base |
|---|---|---|
base.txt |
a b b b |
— |
left.txt |
a b a b b |
inserted one a |
right.txt |
b a b a b b |
inserted a leading b and an a |
A real merge:
$ git merge right # on the 'left' branch, default ort strategy
Auto-merging f.txt
Merge made by the 'ort' strategy. # exit 0, no conflict markers
$ cat f.txt
b a b a b a b b # 8 linesWhy this is unsound. With insertions only, any explicable three-way merge
applies each side's inserted lines at most once, so the result can be no longer
than |left| + |right| - |base| = 5 + 6 - 4 = 7 lines. Git produced 8 — it
invented a duplicate a — and reported no conflict. The repeated run of bs
lets the histogram diff anchor left's insertion and right's insertion on
opposite sides of the ambiguous region, so ort treats them as disjoint and
applies both.
Only histogram misbehaves here; myers, minimal, and patience all merge
soundly on these inputs:
$ for a in histogram myers minimal patience; do \
printf '%-10s ' "$a"; \
git merge-file --diff-algorithm=$a -p examples/minimal/left.txt \
examples/minimal/base.txt examples/minimal/right.txt | tr '\n' ' '; echo; \
done
histogram b a b a b a b b # 8 lines — UNSOUND (git's merge default)
myers b a b a b b # 6 lines — sound
minimal b a b a b b # 6 lines — sound
patience b a b a b b # 6 lines — sound- 3 inserted lines is the floor. Every 1-insert-per-side case up to base length 7 was checked exhaustively (16,872 merges) — none over-applies. With a single new line per side, Git can apply at most both, so it cannot exceed the bound. You need ≥2 lines on one side for the interleave-around-a-repeat mechanism to duplicate.
- Base length 4 is minimal for the 1+2 split over a binary alphabet; lengths 2 and 3 were searched first and yield nothing.
Files in examples/locality/ reproduce Figure 3 of the paper (n = 3). A
prepends 1 2 at the (empty) front region; B changes the trailing 1 2 to 3.
Intuitively these edits are at opposite ends, separated by a long region — yet Git
reports a conflict, independent of how large that region is:
$ git merge-file --diff3 -p examples/locality/A.txt \
examples/locality/O.txt examples/locality/B.txt
... <<<<<<< ... conflict ... # exit 1This is the safe failure mode (an unnecessary conflict), in contrast to the minimal counterexample's unsound one (a silent duplication).
$ ./reproduce.sh # builds throwaway repos in a temp dir and prints resultsSearch for your own counterexamples:
$ python3 fuzz.py 4 # fuzz with seed 4
$ python3 minimize.py # exhaustive minimal search (a few minutes)README.md this file
fuzz.py randomized search for unsound merges (soundness oracles inside)
minimize.py exhaustive minimal-counterexample search
reproduce.sh one-shot reproduction of both examples
examples/minimal/ base/left/right for the minimal unsound merge
examples/locality/ O/A/B for the paper's Figure 3 spurious conflict
- Khanna, Kunal & Pierce, A Formal Investigation of Diff3, FSTTCS 2007. https://www.cis.upenn.edu/~sanjeev/papers/fsttcs07_diff3.pdf
- Glodny, Analyzing and Evaluating the Behavior of Git Diff and Merge, 2025. arXiv:2507.22071.
Apache License 2.0 — see LICENSE. Copyright 2026 Marc John Brooker.