For maintainers and contributors of other open-source projects who want to run a hunt like the one on Apache Lucene.
What we did
AI agents hunted for bugs in Lucene core and its main modules. Anthropic Claude Opus ran the hunt, and OpenAI GPT-5.6 was an independent second model for review and refutation. They used a variety of methods: formal ones (model checking with TLA+, SMT solving, Dafny proofs, bounded model checking), semi-formal ones (exhaustive checks of the real code against a reference on every small input), code reading, and testing (fuzzing, property-based and model-based testing). They checked every finding independently, traced when it started, and wrote each one up with a minimal failing test, a short explainer and fix options. The findings are published on a searchable, filterable site, and upstream progress is tracked in apache/lucene#16937.
In the first two weeks (from late October 2026) the hunt recorded more than 1,250 findings, one per root cause, over 1,000 of them not reported before. Fixes for five of them have been merged upstream, and four more are in open pull requests. The main page has the current numbers.
Principles
Three principles guided the hunt. Under each is what it meant in practice.
1. The Project and Its People Come First
The hunt is only worth doing if it leaves the project and its community better off. Maintainers' attention is the bottleneck of the whole exercise, so everything else is there to spend as little of it as possible and to make their decisions and fixes faster. A huge wall of findings nobody cares about helps no one. In practice this meant three things.
a. Build trust in every finding
The workflow has to earn the maintainers' trust, so every finding is thoroughly verified before a person sees it:
- Minimal failing unit tests.
- Blind verification by agents from a different model family.
- Adversarial checks of whether a finding is really a bug or intended behavior, from several angles: javadocs, code comments, past discussions on related PRs and GitHub issues, the dev mailing list, and the behavior of previous versions (tested, not just read from the code), including whether a change between versions looks expected or accidental.
- A known-or-new check: if others already reported the finding, mark it so.
Tracing a finding through the releases also helps the maintainers directly. They can see how it evolved, which is one more piece of information when they decide its priority and whether it is intended.
These techniques also stop agents from gaming the hunt. Asked to find bugs, an agent can drift toward inflating the number of findings: splitting one bug into several, calling documented behavior a bug, or writing tests that fail for the wrong reason. A minimal failing test, independent reproducers and judges from another model family working in a fresh context, and one finding per root cause catch this. The number of findings is never the goal.
b. Ask "so what?"
Mature or large code bases will always have bugs: some reachable, others latent, and many contrived. Not every unexpected behavior has to be fixed at the same priority. So make the agents reason about reachability and priority, and either mark contrived bugs clearly or drop them.
c. Make the next human step fast
The real work is the fix, and it needs a lot of human input:
- A separate website or tracker works much better than flooding GitHub with AI-generated issues. Make it easy to search and filter (by area, priority, release, method, good first fix), so people find what matters to them quickly. The Lucene hunt's site is one example; its source is on GitHub if you want to reuse it.
- Always respect the project's AI policy. It decides where findings may go and who writes what.
- Explain each finding briefly, with a diagram (and a video where it helps).
- Keep tests minimal. Current models are often right, but in a complicated way.
- Suggest a fix and a regression test, and aim for elegance and minimalism in both, not slop.
2. Do No Harm
This is about security and safety. Agents are very good at finding bugs with security implications for the project itself or for downstream users. Vet those findings carefully and report them through the project's private security channel, so that they don't cause incidents. In practice, every finding got a strict yes-or-no security verdict against the project's security policy, and the ones that might be sensitive were kept off the public list and reported privately first.
3. The Magic Is in the Model
Build for the next model, and trust the model. In a large, breadth-first exercise like this, and especially if you have prior expertise, it is tempting to give very specific prompts. That can backfire and limit the model. We saw this in the Lucene hunt. At first I prompted the model to use only formal verification techniques (hence the bug ids LFV, for Lucene Formal Verification). Going through the output, I saw that it was often forming hypotheses directly from reading the code, and then confirming them with a formal model. So I relaxed the prompt and let the model decide which formal models to use and when, which is why it ended up using so many. In practice, only the outcome and the verification bar are fixed; the path to them stays flexible. The next model will likely be even more capable, and a workflow that is focused on outcomes will carry over to it, or extend easily, instead of needing a redesign.
Methods
Choosing where to look
Picking the next areas mattered as much as the techniques. What worked:
- Step back regularly and look at where the confirmed bugs are, then spend more time in those areas. Bugs cluster.
- Read past bug reports of the project to see where issues usually show up, and which kinds of mistakes keep coming back.
- Ask another model family for the next set of areas to focus on, then check its ideas with real tests before planning around them.
- Go above single methods. Many bugs sit at the component level: how state is passed or assumed between layers, what one component expects the next one to have done, and how components interact under concurrency. These often need a formal model of the protocol, or fuzz and stress testing of the real code, rather than a check of one method.
When the hunt runs dry
Yield drops as the easy areas are covered. Before stopping, try new angles. The verification bar stays the same:
- Map the coverage. Count findings and planned work per package or component, and look at the rich, widely used parts with few of either.
- Follow fresh code. Review commits merged since your last pass and new features in the latest release. New code has new bugs.
- Compare versions. Run the same seeded inputs through two releases and explain every difference the changelog does not.
- Mine new fixes. Every fix that lands upstream, from you or from others, is a pattern to look for elsewhere.
- Change the level or the method. Move from single methods to components and protocols, or from code reading to exhaustive checks, a formal model or fuzzing, and the other way round.
- Look downstream. Bug reports in projects built on yours often trace back to it.
- Ask another model family for new angles, and have critics from both families review the new plan.
If the new angles also come back empty, say that the area is dry. Don't lower the bar to keep the count up.
Techniques and tools that worked
These are the techniques and tools that worked for Lucene, a Java code base; the site's method filter shows what each one found. In another language the tools will be different, so let the model choose the ones that fit your language and build (its fuzzers, property-based testing, model checkers, proof tools and sanitizers). The ideas carry over better than the tool names.
| Method | Good for | Notes |
|---|---|---|
| Exhaustive differential checks | Code with an exact spec | Run the real build against a reference on every input up to a small bound. The most productive method. |
| Code reading while modelling | Anything | Writing a model forces every branch into the open. |
| Contract audits | Classes with rich contracts | List what the contract promises and check each item. Mostly Low-priority finds. |
| SMT (Z3, cvc5) | Arithmetic at the limits: overflow, rounding, NaN, signed zero | Re-run every model the solver returns as a test. |
| TLA+ and TLC | Concurrency and lifecycle with two or three actors | The trace becomes the test. |
| Dafny, JBMC and CBMC | Small kernels | Mostly useful for aiming the other checks. |
| Metamorphic checks | Queries, merges, batching | Results must not change when clause order, segment order or batching changes. |
| Fix-sibling mining | Recent fixes | Look for the same mistake elsewhere in the code. |
| Mutation testing | Test gaps | A pointer only: confirm each survivor through the public API. |
| Testing baselines | Everything | Model-based testing, fuzzing, stress and static analysis. Few first signals, but model-based testing found some High-priority ones. |
How a finding moves through the pipeline
- Plan: split the code into units, each with its files, contract, method and known bugs. Critics from both model families review the plan.
- Hunt: an agent models the code and writes a failing test on the unmodified build.
- Dedup against the findings already recorded.
- Verify in parallel: a separate agent writes its own test, a reviewer from the other model family tries to refute the finding, and another agent argues that the behavior is intended.
- Judge: confirm only if the independent test fails for the stated reason and no refutation holds.
- History, prior reports and a security check.
- A final no-noise review.
- Write-up: a short brief and a diagram, fact-checked by both model families.
- A person decides what to do with it, and writes anything that goes upstream.
Use it in your project
HOWTO.md is the same method written as instructions for an AI agent. Give it to your agent with a local checkout of your project, your name as the person it reports to, and a private folder for security notes. The agent works out the rest (the project, its version, build and policies) by itself.