Formal models and scripts

The small text models (TLA+, Alloy, SMT-LIB, Dafny) and Python scripts (SMT queries, exhaustive checkers, scanners) of the parts of the hunt that made a public finding. A unit lists the findings its files were used for; that a unit holds a model does not mean the model gave the first signal (each finding's record names its first finder).

UnitToolsFilesFindings
analysis-benchmark-backward-codecs-javadoc-examples-compile-on-mainPython2LFV-1041, LFV-1040
analysis-factory-javadoc-examples-and-resource-files-build-as-documentedPython1LFV-931
analysis-loaders-release-streams-and-temp-files-on-failureTLA+/TLC6LFV-1006, LFV-1010
analysis-rule-tables-second-batchPython1LFV-688
analysis-spi-chain-fuzzPython1LFV-439
ascii-folding-table-vs-unicode-character-databasePython1LFV-818
assert-only-input-checks-sweep-siblings-of-16919Python1LFV-1013
bitsets-livedocs-acceptdocsPython4LFV-139, LFV-147, LFV-137, LFV-133
bkd-write-niche-configsPython1LFV-613
boolean-rewrite-dispatchPython2LFV-103
bulk-overload-precondition-matrixPython1LFV-475
bytebuffers-output-block-expansion-recycler-and-view-aliasingTLA+/TLC4LFV-836
cjk-compiled-dictionary-source-round-tripPython1LFV-717, LFV-710
classificationPython5LFV-382, LFV-380, LFV-395, LFV-388
codec-format-javadoc-grammar-overflow-liv-cfe-extension-tablePython4LFV-972, LFV-970, LFV-974, LFV-971
codecreader-wrappersPython3LFV-278, LFV-318, LFV-285
collation-pkginfo-danish-example-sort-setsort-after-16904Python1LFV-1085
columnar-addbatchPython1LFV-097, LFV-101, LFV-094
concurrent-collector-managersPython1LFV-202
core-fst-package-examples-compile-and-print-documented-outputsPython2LFV-1027
cosine-zero-query-vector-silent-empty-results-known-15540-row-or-dnpPython1LFV-1141
count-stats-modulesPython1LFV-428
count-totalhitsAlloy1LFV-086
datainput-impls-stringsPython1LFV-107
deleteall-during-addindexes-keeps-imported-field-schemaTLA+/TLC1LFV-1074
directio-nrtcaching-dirsPython1LFV-226
dismax-synonym-combinedPython1LFV-272
distance-feature-pruningSMT-LIB (Z3/cvc5), Python8LFV-379
docandscorequery-public-factory-count-and-iterator-contractsPython1LFV-955
docterms-range-scorer-float-ordinals-above-2p24Python1LFV-1108
document-field-factoriesPython1LFV-140
docvaluesstats-sorted-double-stats-decode-sortable-doubles-as-raw-bitsPython2LFV-1129
dv-norms-cursor-coherencePython3LFV-415, LFV-419, LFV-418
dv-range-primary-sort-shortcut-ignores-sort-typePython1LFV-1047
dw-flush-control-deletequeue-tlaTLA+/TLC15LFV-473, LFV-474, LFV-471
dwfc-nextpendingflush-stale-fullflush-stock-reproTLA+/TLC5LFV-1045
executor-pluggable-behaviour-sweepTLA+/TLC10LFV-637
explanation-formula-strings-vs-their-own-operand-valuesPython2LFV-922, LFV-921, LFV-920
expressions-shallow-large-expression-escapes-documented-exceptionsPython1LFV-906
facet-top-ordinal-queues-nan-and-special-value-orderSMT-LIB (Z3/cvc5), Python12LFV-825, LFV-820
facets-topn-and-topndims-queues-presized-uncappedPython2LFV-994, LFV-983
facetset-dimrange-and-rangeonrange-exclusive-bound-signed-zero-gapPython2LFV-1131
failed-commit-then-crash-durability-single-faultTLA+/TLC1LFV-839
feature-saturation-sigmoid-cancellationSMT-LIB (Z3/cvc5)10LFV-898
featurefieldSMT-LIB (Z3/cvc5)8LFV-258
frequent-terms-span-rewrite-size-edges-16484Python1LFV-944
frozen-updates-apply-merge-carryover-tlaTLA+/TLC4LFV-596
function-queries-bmwSMT-LIB (Z3/cvc5), Python15LFV-211, LFV-203, LFV-189, LFV-214, LFV-221
fuzzy-levenshteinPython1LFV-350
geo-tessellator-shapesPython1LFV-204
geo-text-parsers-deep-nesting-vm-errors-siblings-of-16423Python1LFV-952
grouping-offset-plus-limit-overflowPython3LFV-964, LFV-958, LFV-960
groupingsearch-cache-limit-applied-per-slice-10-6Python1LFV-910
hardlink-copy-unwrap-bypasses-intermediate-directory-wrappersTLA+/TLC9LFV-912
hnsw-10x-merge-reuse-maxconn-mismatchPython1LFV-811
hnsw-merge-reusePython1LFV-160
hnsw-parallel-repair-tlaPython1LFV-458
htmlstrip-tag-open-name-class-vs-html-tokenizer-referencePython1LFV-878
hunspellPython3LFV-373, LFV-377, LFV-374
hunspell-set-encoding-names-vs-c-hunspell-referencePython2LFV-933, LFV-928
hunspell-synthetic-dictionary-differentialPython3LFV-731
hunspell-wordform-generator-munch-differentialPython3LFV-641, LFV-634
indexeddisi-dv-bulkPython3LFV-169, LFV-165
indexfiledeleter-refcount-tlaTLA+/TLC6LFV-472
indexingchain-schemaAlloy, Python10LFV-118, LFV-116, LFV-127, LFV-124
indexrearranger-and-pkindexsplitter-failed-run-cleanupPython1LFV-1011
indexsorted-leaf-delegate-points-work-after-mixed-leafTLA+/TLC15LFV-1088
indri-query-family-composite-score-boost-visitor-explain-lawsPython1LFV-874, LFV-872, LFV-871, LFV-875
iw-blocking-calls-watchdog-failure-visibilityTLA+/TLC8LFV-648
iw-forcemerge-wait-protocol-tlaTLA+/TLC11LFV-590, LFV-587, LFV-586, LFV-592
iw-from-reader-commit-leaf-sorted-reader-pairs-wrong-segmentsPython1LFV-1062
iw-hasuncommittedchanges-read-order-raceTLA+/TLC8LFV-1060
japanese-completion-fifoPython1LFV-346
javadoc-package-and-overview-examples-call-removed-apis-siblings-of-16904Python4LFV-989, LFV-980, LFV-992, LFV-987, LFV-984, LFV-988
knn-query-layerTLA+/TLC11LFV-106, LFV-114, LFV-117, LFV-125, LFV-123
kuromoji-completion-romaji-map-vs-hepburn-kunrei-wapuro-tablesPython4LFV-849, LFV-850, LFV-848, LFV-854
latlon-geo-queries-referencePython1LFV-578
legacy-int7-int4-scalar-quantized-scoring-fp-smtPython1LFV-841
lmdirichlet-mu-zero-limit-and-multisimilarity-norm-combsumPython1LFV-902
locks-pending-deletesTLA+/TLC4LFV-343
lruquerycache-partitioned-clear-and-callback-serializationTLA+/TLC27LFV-991, LFV-1001, LFV-1000
memory-bitset-collector-managerTLA+/TLC1LFV-348
merge-on-commit-refresh-tlaTLA+/TLC1LFV-502
migrate-upgrade-example-forcemerge-keeps-old-formatPython1LFV-1030
misc-reorder-splitPython2LFV-531
monitor-lifecycle-persistence-mbtTLA+/TLC8LFV-499, LFV-501
monitor-matcher-agreementPython3LFV-852, LFV-853, LFV-856
monitor-presearcherTLA+/TLC1LFV-332
never-judged-backlog-closure-low-and-not-a-bugTLA+/TLC10LFV-1061, LFV-1059
ngram-tokenizers-maxgram-above-input-lengthPython1LFV-1007
nontragic-indexing-failure-loses-acknowledged-opsPython1LFV-1090
nrt-reference-managersTLA+/TLC18LFV-250, LFV-252, LFV-312, LFV-264, LFV-309
numeric-dv-bulk-valuesPython2LFV-381
numeric-string-version-utilsSMT-LIB (Z3/cvc5), Python11LFV-327, LFV-323
offline-sorterTLA+/TLC6LFV-384, LFV-357
osq-quantization-newPython1LFV-084
overflow-at-scale-2SMT-LIB (Z3/cvc5), Python16LFV-394, LFV-397, LFV-401, LFV-387, LFV-383
packed-ints-monotonicPython1LFV-148
parallel-reader-advertises-index-sort-of-shadowed-sort-fieldPython3LFV-981
pointrange-rewrite-fieldexists-ignores-leaves-without-pointsPython1LFV-1109
postings-lucene104Python2LFV-183, LFV-170
priorityqueue-topdocs-mergeDafny4LFV-262, LFV-267, LFV-294
queries-mlt-commonterms-referencePython1LFV-571, LFV-559, LFV-553
query-cache-correctnessTLA+/TLC9LFV-308, LFV-320, LFV-336
query-object-contractsPython1LFV-304
queryparser-classicPython3LFV-319, LFV-284
queryparser-flexible-simple-xmlPython2LFV-356, LFV-398
range-bound-cross-pathPython1LFV-409
reader-open-leaf-sorter-failure-leaksTLA+/TLC1LFV-1067
reqexcl-bulkscorer-excluded-run-skip-16669Python1LFV-1044
rescorers-nearest-and-rescoretopn-presized-by-unbounded-topnPython2LFV-997, LFV-995
rescoretopn-negative-rescore-values-maxscore-hangSMT-LIB (Z3/cvc5), Python34LFV-1015, LFV-1016
searcherlifetime-prune-orderTLA+/TLC9LFV-1066
sloppymath-and-geo-distance-documented-error-boundsPython3LFV-771
slow-codec-reader-vector-metadata-answered-past-wrappersAlloy2LFV-911
smartcn-hhmm-segmentation-referencePython1LFV-709
snapshot-deletion-policies-commit-retention-model-basedTLA+/TLC1LFV-890
sort-leafstart-hitsthreshold-before-setscorer-points-intersect-16857TLA+/TLC9LFV-1057
sortednumeric-double-float-sortable-vs-raw-decoding-facet-and-joinPython1LFV-1111
sortednumeric-dv-updateAlloy1LFV-134
sorters-selectorsPython1LFV-372
span-containing-within-lockstep-misses-nested-little-spansTLA+/TLC17LFV-909
spatial-extrasPython2LFV-369
spatial-extras-composite-and-prefix-tree-query-cross-checkPython1LFV-705
spatial3d-geometryPython1LFV-209
spellchecker-candidate-budget-int-overflowPython3LFV-986, LFV-996
store-cross-impl-differentialPython1LFV-492
storedfields-compressingPython3LFV-172, LFV-186, LFV-163
study-automaton-verificationTLA+/TLC, Dafny12LFV-049, LFV-055, LFV-057, LFV-062
study-bkd-points-proofDafny, Python15LFV-006, LFV-050, LFV-059
study-fst-verificationAlloy, Dafny, Python7LFV-052, LFV-007, LFV-070, LFV-067
study-hnsw-concurrent-mergeTLA+/TLC, Python36LFV-005, LFV-061, LFV-068
study-overflow-at-scaleSMT-LIB (Z3/cvc5), Python34LFV-048, LFV-003, LFV-058, LFV-066, LFV-069
study-quantization-smtSMT-LIB (Z3/cvc5), Python22LFV-047, LFV-046, LFV-064, LFV-079, LFV-065
study-search-concurrency-modelTLA+/TLC, Python16LFV-045, LFV-053, LFV-054, LFV-077, LFV-056
study-simd-equivalenceSMT-LIB (Z3/cvc5), Python60LFV-044, LFV-071
study-similarity-impacts-smtPython13LFV-063, LFV-072, LFV-073
study-topk-pruning-proofSMT-LIB (Z3/cvc5), Dafny, Python16LFV-060
subtoken-offset-containment-sweepPython1LFV-603
suggester-lookup-num-overflow-and-presizePython3LFV-999, LFV-998, LFV-1003
suggestersTLA+/TLC7LFV-263
taxonomy-index-pair-tlaTLA+/TLC12LFV-481, LFV-489
taxonomy-writer-concurrent-addTLA+/TLC9LFV-521, LFV-520, LFV-512
termvectors-compressingPython1LFV-244
timeout-partial-resultsPython1LFV-465
trydvupdate-bypasses-ram-buffer-unbounded-heapPython1LFV-1075
twin-family-static-diffPython1LFV-427
uax29-word-boundaries-referencePython2LFV-734
unicode-conversionsPython1LFV-385
upstream-delta-columnar-dense-vector-batchPython1LFV-579
vectorutil-providersPython1LFV-138
wand-blockmax-boundsPython1LFV-104, LFV-113
word2vec-synonym-provider-vs-exact-cosine-referencePython1LFV-870

Snapshot of 2026-11-03. AI-assisted; not yet triaged by a human Lucene committer. Feedback: open an issue in lucene-ai-bug-hunt.