AI-assisted · Apache Lucene
An AI-assisted hunt, run with Claude Opus 5.5 and GPT-5.6, looks for Lucene bugs using a variety of tools and techniques, like formal verification (TLA+/TLC model checking, Alloy, Z3/cvc5 SMT solving, Dafny proofs, bounded model checking), fuzzing, and model-based and differential testing, and confirms each finding with a minimal unit test. The search is only part of the work: a person still has to triage every finding and design the right fix.
This page is a dated snapshot of AI-assisted work. The findings the hunt made and confirmed went through AI-run checks. This is an independent list: per the Apache Lucene project’s AI policy, nothing here is filed in Lucene unless a person files it by hand.
On this site: all repro folders · formal models and scripts · the table as CSV · as JSON.
Snapshot: 2026-11-03
All counts and charts on this page cover new findings only. 864 findings are new: the prior-report search found no earlier report of them. Another 290 findings the hunt made were already known upstream; they are not included in any count, chart or method credit here. To see them, tick “Show findings already known upstream” above the findings table. Of the new findings, 2 have their details withheld pending security review; they still count in every number here.
1 finding triaged by a Lucene maintainer as won't fix is hidden by default; to see it, tick “Show findings maintainers triaged as won't fix” above the findings table.
Findings marked new in 10.6 are in Lucene 10.6.0 (released 2026-10-29) but not in 10.5.2.
One row per root cause: the code a minimal fix changes; symptoms with the same fix site count as one finding. Choose an ID to open the finding’s full record. Under each ID: new, or known upstream with the item that already covers it.
How priority is decided: each finding is High, Medium or Low, and each finding shown in full has a rank across those findings (1 = most important). It is a judgement, not a formula, over how far the finding reaches, core or a module, usual inputs or rare ones (such as Integer.MAX_VALUE sizes), how severe the failure is, default or opt-in configuration, and released or unreleased code. One model ranks the findings and a model from another family gives a second opinion.
The table lists findings in rank order. Each finding’s priority note says why it sits where it does: hover, focus or tap the badge. Beside the badge is the impact class, the worst effect a user can see; under it, the likelihood, how realistically a user runs into the problem.
First affected release, then the age of the affected code once it is a year old: whole years since the introducing commit, or since the first affected release when the commit date is not known. “About N years” below 10, “over N years” from 10. No age while no release is affected (unreleased, or none affected). The age is counted on your device’s clock, and the full record names its basis.
The second line names the introducing commit or pull request.
First signal only: a finding counts under the method named in the first clause of its found-by text, so a method that reached it later does not count (How findings are found, below). A finding whose first clause names two methods counts under both.
Formal methods: TLA+/TLC, Alloy, P, Dafny, Z3/cvc5, JBMC, JPF or KeY/OpenJML.
Testing baselines: randomized/MBT, fuzzing/PBT, static analysis or stress.
Other methods: exhaustive checks of the real jar, the obligation audit and code reading.
Rows with details withheld are not credited to any method.
New: the prior-report search found no earlier report, issue, pull request or mailing-list discussion of the finding; reports filed from this list (tracked in apache/lucene#16937) count as new. Known upstream: the prior-report search found a report of the same finding by others. New means no earlier report was found (a keyword search; private reports are not visible).
Findings already known upstream are left out of every count on this page. Shown, they follow the new ones, muted, each with the upstream item that already covers it. The counts in the menus cover the findings on show.
Formal methods are one of the project’s main techniques, not the only one: they run side by side with testing baselines, and some findings were first spotted by reading the code. The hunt plan splits lucene/core and the important modules (sandbox excluded) into units; each unit pairs a primary formal method with a non-formal baseline and an oracle. Of the 862 new findings the hunt made that are shown in full, a formal tool’s own output gave the first signal for 45, a semi-formal check for 492, code reading or other testing for 298 and a testing baseline for 27.
Every registry entry records its first finder: the method whose output gave the first signal. Finders fall into 4 tiers:
The lists under each method are computed from each entry's found-by text. First signal is a method named in its first clause, credited only when the finding’s tier allows it (a formal tool for a formal finding, its own output, or a semi-formal one, a witnessed hypothesis; a testing baseline for a finding of the baseline tier), so a tool a record only mentions gets no credit; also reached is a method that re-found the finding later, often after being told which class to look at, so it is not an independent discovery.
The lists and the tier chart credit new findings only: a method gets no credit for a finding that was already known upstream. The Method filter above the findings table uses the same first-signal credits: “all formal methods” shows the findings of the formal tier and “all testing baselines” those of the baseline tier, as in the tier chart.
formal
Write a small state machine of a protocol (indexing threads, a merge, a reader reopen, a search barrier) and let TLC visit every reachable state up to a bound. When an invariant breaks, TLC prints the shortest sequence of steps that breaks it, and that trace becomes a JUnit test on the real jars.
TLA+ tools 1.8.0 (TLC)
Computing from the registry.
formal
Describe the data (segments, generations, pending updates) as relations with constraints and ask the analyzer for an instance that violates a property. It searches every instance up to a size bound with a SAT solver and returns a small counterexample.
Alloy 6.2.0 with the SAT4J solver
Computing from the registry.
formal
Model components as communicating state machines and let the P checker explore interleavings with its random and PCT (probabilistic concurrency testing) schedulers. It samples schedules rather than proving anything; a failing schedule replays exactly.
P 3.1.0 (random and PCT schedulers)
Computing from the registry.
formal
Write the algorithm and its specification in Dafny; the verifier must prove every step for all inputs. An obligation that will not go through points at a case the real code may get wrong, or at a precondition the real code does not guarantee; either one aims a test at the real jar.
Dafny 4.11 with Z3 4.12.2
Computing from the registry.
formal
Encode one expression exactly as Java evaluates it, as 32- or 64-bit two's-complement integers or IEEE-754 floats, and ask the solver for inputs within the documented limits that overflow, round the wrong way or produce NaN. The answer is a concrete input or a proof that none exists.
Z3 4.12.2 and 5.3.1, cvc5 1.4.2; candidate expressions from a CodeQL inventory
Computing from the registry.
formal
Unroll the loops of real Java bytecode to a fixed depth and check every assertion, array access and arithmetic step for all data values. On Java 25 it handles kernels and hand-written slices.
JBMC/CBMC 6.11.0
Computing from the registry.
formal
Explicit-state search of small Java programs: every thread interleaving of an extracted slice, with race and assertion checks.
jpf-core, java-17 branch
Computing from the registry.
formal
Deductive verification of Java code against JML contracts. On Java 25 both accept only hand-written slices or ports, so here they gave proofs on kernels and re-finds of known findings rather than first finds.
OpenJML 21.0.29, KeY 3.0.0 and 2.12.3
Computing from the registry.
semi-formal
Run the shipped Lucene jar against an exact reference implementation on every input in a bounded space (every small automaton, every Unicode code point, every small point layout) and report any disagreement. The shipped code itself runs, so nothing is lost in transcription; the bound and the reference are the only gaps. Some harnesses in this group sampled their bounded space at random instead of covering all of it; the records of their findings say so.
custom exact-semantics checkers
Computing from the registry.
semi-formal
List the obligations a proof would need (for example, which lock guards each field on each path) and check each one against the code. A failed obligation is turned into a test.
model-assisted review
Computing from the registry.
non-formal baseline
Drive IndexWriter and readers with random operation sequences while a simple in-memory model predicts every result; a divergence, an exception or a CheckIndex failure is a finding, shrunk to a short sequence.
stateful random tests with an in-memory model and CheckIndex as oracles
Computing from the registry.
non-formal baseline
Coverage-guided fuzzing and property-based tests feed generated inputs to parsers, automata and data structures and compare against an oracle such as java.util.regex, java.util.BitSet or a brute-force reference.
Jazzer, jqwik 1.10.2
Computing from the registry.
non-formal baseline
Pattern-based analyzers flag local contract violations (an ignored return value, an inconsistent hashCode, integer overflow) and list candidate expressions for the SMT queries; every report is confirmed with a test before it counts.
CodeQL 2.27.3, Error Prone 2.50.0, SpotBugs 4.10.5, PMD 7.28
Computing from the registry.
non-formal baseline
Multi-threaded stress with a linearizability or sequence-number oracle, plus tools that control or replay thread schedules.
Lincheck 3.7, Fray 0.9.0, JCStress 0.16
Computing from the registry.
non-formal
Writing a model forces every branch to be stated, and the odd one stands out. Many findings were first spotted this way (the list below counts them), one by replaying a published result; each was then confirmed by an executed test.
no tool; often while writing a model or an oracle
Computing from the registry.
A new candidate goes through the steps below, in order. It needs an executable repro; the only exception the hunt's rules allow is a proof-only finding that this hardware cannot run, and it ranks below executed ones. All of these checks are AI-run.
This site says “findings” rather than “bugs”. Each finding is a behaviour the checks reproduced with a minimal failing test, not a claim that Lucene must change: some may turn out to be intended behaviour, a documentation gap or a trade-off made on purpose, and some real bugs are so rare or contrived that they may not need a fix (LFV-196 is an example). The AI-assigned priorities put most findings at Low, and a person verifies a finding before anything is filed upstream.
Computing from the registry.
A JUnit test asserts the documented behaviour and fails on the stock jars of Lucene main (ea57360912ed) with a fixed seed, run with assertions on and off, because production runs with them off. The hunt’s repros use no shadow classes and no reflection in the failing assertion; a few repros from the earlier study read a private field by reflection or need extra JVM instrumentation, and their repro pages say so. The same test then runs against released jars to find the oldest affected release.
AI reviews, independent of the AI that made the finding, rebuild the evidence and try to refute it: re-run the repro, re-read the contract, check the trigger is legal. A reviewer from another model family (OpenAI GPT-5.6) looks for a modelling error, intended behaviour, an illegal trigger, a duplicate or a misread result, and, for most findings, a skeptical audit looks for overclaims (each record says whether it had one). A refutation is answered by re-running the repro and, when it argues contract, scope or intent, by a written adjudication; the reviewer disputed some findings, could only read the code for others, and gave no verdict on a few, and each record says which.
A checker argues the behaviour is intended, from the javadoc, CHANGES, MIGRATE, upstream tests and the introducing pull request's discussion. Without a stated contract a finding is at most a documentation defect; an explicit “won't fix” or “by design” means it is not a bug.
git blame and git log -S on a full-history clone find the introducing commit and pull request, a commit-level bisect runs where reading is not enough, and release tags give the first affected version. Facts are marked [exec] when executed and [read] when read from code or history.
Read-only searches of GitHub issues and pull requests (several phrasings, plus open pull requests that touch the same files), the old JIRA archive (LUCENE-NNNN), and the dev@ and java-user@ mailing-list archives. A finding someone else already reported keeps its own status, the upstream column names their item, and it is marked known upstream: listed apart and left out of every count.
The brief records what happens, where and when, a minimal example, version details, how it was found and the fix options. A claim re-check verifies every disputed or single-source claim by execution or reading and records a verdict per claim.
A finding is new when the prior-report search finds no earlier report, issue, pull request or mailing-list discussion of it. The search is automated and keyword-based, and private reports (to security@, for example) are not visible, so new means that no earlier report was found. Reports filed from this list (tracked in apache/lucene#16937) count as new: filing a finding upstream does not make it known. When the search finds a report of the same finding by others, the finding is known upstream.
Known findings that the hunt rediscovers are still useful: a rediscovery adds an executed repro and often a fresh analysis to the existing report. They are left out of every count, chart and method credit on this page, because the hunt cannot show that it found them independently of what was already published: the earlier report may have shaped the models' prior knowledge or the material they searched. The status board names how many there are; the findings table lists them only on request.
| Status | Meaning | Findings |
|---|---|---|
| candidate | Reported once; no independent check yet. | — |
| reproduced | An executable repro fails on main; no independent verdict yet. | — |
| confirmed | Independent checks agreed (a majority, or a written adjudication). | — |
| briefed | A brief or fact sheet exists, plus independent checks of it. | — |
| documented | A per-finding doc exists (see Learn about a finding). | — |
| filed | An upstream issue or pull request has been filed for this defect, as a report or as an issue for discussion. The “Filed or triaged” tile counts these findings together with the ones a maintainer has triaged. | — |
| withheld | Details withheld pending security review; the status is not shown. | — |
Until a person has checked it, an AI finding is a lead, not a result. Before a finding goes upstream a contributor verifies it again and designs the fix; that is the hard part of the work, and each artifact the AI tools produce is there to make one step of it shorter.
| Step | What the contributor does | What the AI tools hand over |
|---|---|---|
| Verify again | Runs the repro on a clean build of main, with assertions on and off, and reads the failing assertion. | A minimal repro: one small JUnit test with a fixed seed, and the exact command that runs it. |
| Bug or intended | Decides whether the documented contract really promises the other behaviour. | The doc’s case that it is not intended, and the devil’s-advocate check with the javadoc, CHANGES entries and pull-request discussion it rests on. |
| Upstream history | Checks that nobody reported or fixed it already, and where it came from. | The prior-report check (what was searched, when, and what turned up) and the code history: the introducing commit and the first affected release. |
| The right fix and its tests | Chooses the change a committer would accept, at the right layer, and a test that fails before the change and passes after it. | Fix options with their trade-offs; the repro is the starting test. |
| Discuss and file | Writes the issue or pull request in their own words, under their own name, and answers the review: Lucene’s AI_POLICY.md asks that issues, pull requests and comments be written by a human. | A short doc to work from and, for most findings, a GitHub-ready diagram (a still image). |
JDK 25: Lucene main requires Java 25, and the hunt ran on 25.0.3. Lucene main at
ea57360912ed (version 11.0.0-SNAPSHOT), built with
./gradlew --no-daemon assemble, which leaves
lucene/<module>/build/libs/lucene-<module>-11.0.0-SNAPSHOT.jar.
Each repro is a JUnit test, usually extending LuceneTestCase, that asserts the documented
behaviour and so fails while the reported behaviour is present. Compile it against lucene-core, lucene-codecs and
lucene-test-framework plus the test framework's dependencies, and run it with the JUnit Platform console
launcher, whose vintage engine runs LuceneTestCase tests.
For a production-like run, replace -ea -esa with -da -dsa -Dtests.asserts=false.
For a release, swap the three Lucene jars for that release's jars from Maven Central and use its own test
dependencies (10.5.2's test framework uses randomizedtesting 2.8.1, junit 4.13.1 and hamcrest 2.2).
A failing test is the finding reproducing; the failure message states expected against actual. A rerun with the same seed replays the same random choices.
# Lucene checkout at ea57360912ed, built as above
L=/path/to/lucene; V=11.0.0-SNAPSHOT
CP=$L/lucene/core/build/libs/lucene-core-$V.jar
CP=$CP:$L/lucene/codecs/build/libs/lucene-codecs-$V.jar
CP=$CP:$L/lucene/test-framework/build/libs/lucene-test-framework-$V.jar
CP=$CP:randomizedtesting-runner-2.9.2.jar:junit-4.13.2.jar:hamcrest-3.0.jar
CP=$CP:junit-platform-console-standalone-6.1.3.jar
javac -d classes -cp "$CP" TestTheBug.java
java -ea -esa --add-modules jdk.incubator.vector \
--enable-native-access=ALL-UNNAMED -Dtests.seed=DEADBEEF \
-cp "classes:$CP" org.junit.platform.console.ConsoleLauncher \
execute --select-class org.apache.lucene.index.TestTheBugReplace the test name and package with the finding's own. Every finding shown in full links its repro folder below; a finding with a doc also links its doc's repro section. The repro index lists every folder: repro/index.html; the formal models and scripts are under models/, and the table is also data: CSV, JSON.
Each documented finding has its own page on this site. A page holds:
Security-sensitive means in scope of Lucene’s SECURITY.md; those are reported privately first. This site withholds them, and also the findings whose automated security reviews disagreed (held back until a person decides) and findings that are part of such a finding: the table keeps only their ID, module, priority tier and whether they are new or known upstream, with no title, description, repro or doc, and they still count in every total. Security-sensitive bugs go privately to security@lucene.apache.org first, before anything public. Every other finding is an ordinary public finding and carries no security mark.
Lucene's AI_POLICY.md asks that issues, pull requests and comments be written by a human. This site is AI-assisted and files nothing upstream: the AI tools produce findings, check them and draft fact sheets; they never post to GitHub, JIRA or the mailing lists, and use GitHub search read-only. A person writes every upstream report in their own words; a brief is a fact sheet, not text to paste.
Where others already reported a finding, the upstream column names their item. Such a finding is known upstream and is not counted. Contributors are referred to by GitHub handle, as they/them.