Isabelle Testing Project -- Findings Summary This document summarises the findings reported in "Testing the Verifier: Automated Testing for Isabelle" together with the project ownership mapping used in this repository. Abstract. This initial report summarises the investigation and gives each student space to describe their individual experience of the process. A more concise and synthesised report, intended for publication as a research paper, is planned as future work. We present a fuzzing-based approach for testing Isabelle by targeting components that interact with its trusted core. Over six months, four students investigated different subsystems and uncovered 25 distinct anomalies. We reported 20 findings to the developers, 13 of which were confirmed, and 12 were subsequently fixed in response to our reports. We also submitted seven patches, resulting in six accepted pull requests and improving the quality of the broader Isabelle ecosystem beyond its core. Acknowledgements. We thank Larry Paulson and Fabian Huch for discussions and feedback that helped shape this project.We thank King's College London, Department of Informatics, for supporting this project under Knowledge Transfer Projects (KEP) 2025/2026 UG. Evaluation The evaluation tested four Isabelle ecosystem components using fuzzing, differential testing, and targeted whitebox analysis. Each subsystem employed tailored automated testing pipelines with custom harnesses, input generation, coverage-guided exploration, and manual validation. Findings were reported upstream, with developer confirmation, accepted patches, and code coverage used to assess the effectiveness of each methodology. Findings Ownership Findings Subsystem Student PRs By Student #1--5 Poly/ML Lexer (x86) Enzo Bestetti Commits: fc8748, 2a1c2ab #6--8 Poly/ML ARM64 Aravinth Kaneshalingam PR #294 (waiting to merge). #9--19 Isabelle/jEdit Bartosz Gowacki - #20--24 Sledgehammer Jiangjing Xu PR #103, PR #106, PR #106, ebb7430 (direct suggest ack in the commit) Issues #10, #24, and #25 were detected by our approach but had already been reported by others. All other confirmed issues were never reported before we did. Additional repositories: https://zenodo.org/records/19593541 https://zenodo.org/records/19593553 https://zenodo.org/records/19593519 https://zenodo.org/records/19696191 https://zenodo.org/records/19899187 https://github.com/BGlowacki-kcl/Isabelle_dissertation_Bartosz/tree/main/differential/bug_reports (also attached as a zip here) https://github.com/aravinth-kanesh/polyml-fuzz (also attached as a zip here) https://github.com/Xujiangjing/fyp-isabelle-fuzz (also attached as a zip here) https://github.com/enzozbest/polyfuzz (also attached as a zip here) Findings Summary The component-level breakdown reveals the following. Poly/ML lexer has the broadest spread across all categories, with one new issue, one confirmed issue, three fixed issues, and four marked as WONT FIX, which includes duplicate bugs, false positives and minor bugs that the maintainers found irrelevant to the reliability of the platform (e.g not a clear enough error message). While the sledgehammer shows the strongest resolution trend. All six recorded issues are fixed, with no remaining new, confirmed, or WONT FIX items. This points to focused maintenance and effective closure of known problems. Isabelle/jEdit stands out because most of its issues are classified as WONT FIX. With 8 in that category and only 3 fixed, the pattern may indicate design limitations, low-priority requests, obsolete reports, or issues considered too costly relative to their impact. The absence of new or confirmed items could also mean that its backlog is relatively stable. Component New Confirmed Fixed WON'T FIX Poly/ML lexer 1 1 3 4 Isabelle/jEdit 0 0 3 8 Sledgehammer 0 0 6 0 Overall, the data suggest that Sledgehammer has the healthiest issue-resolution profile, Poly/ML lexer has the most mixed workload, and Isabelle/jEdit carries the largest set of unresolved but intentionally closed issues. The main follow-up area is understanding the connection between the testing technique used and the component bug discovery performance. Public Bug Reports, Pull Requests and References [THIS IS A FIRST DRAFT! - PLEASE CHECK NEWER VERSIONS] Here is the data formatted into a clean Markdown table with consistent column alignments Finding Component Report venue Status Evidence TODO #1 Poly/ML lexer X86 public mailing list Confirmed Confirmed bug with a proposed fix; no fix approved. - #2 Poly/ML lexer X86 GitHub Issue #256 Fixed Commit fc87489 + email [link] - #3 Poly/ML lexer X86 GitHub Issue #258 Fixed Commit 2a1c2ab + email [link] - #4 Poly/ML lexer X86 N/A WON’T FIX Private communication regarding poly/ml lexer behaviour (2026), email correspon-dence between David Matthews and Enzo Bestetti - #5 Poly/ML lexer X86 N/A Not reported Informational observation; likely intentional parser deviation Remove from the final list of bugs #6 Poly/ML ARM64 GitHub Issue #271 Reported A fix was suggested as PR #294. - #7 Poly/ML ARM64 GitHub Issue #273 WON’T FIX Remove from the final list of bugs #8 Poly/ML ARM64 GitHub Issue #272 Fixed Commit cf7b84a (Input 1) - #8 (dup) Poly/ML ARM64 GitHub Issue #274 Duplicate The maintainer confirmed the shared root cause. Closed as a duplicate of #272 Remove from the final list of bugs #9 Isabelle/jEdit Mailing list [link] [additional data link] Fixed Maintainers committed a patch in response to our report that prevents the observed behaviour from happening. - #10 Isabelle/jEdit NA Fixed Old bug. Fixed (before we reported it) on the trunk [link]. - #11 Isabelle/jEdit Mailing list Not Reported Patch submitted to developers Remove from the final list of bugs #12 Isabelle/jEdit Mailing list [link] [additional data link] Fixed Maintainers committed a different patch in response to our report that prevents the observed behaviour from happening - #13 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #14 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #15 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #16 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #17 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #18 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #19 Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive Remove from the final list of bugs #20 Zipperposition GitHub Issue #102, [Mailing list], and [Mailing list 2] Fixed PR #103 - #21 Zipperposition GitHub Issue #104 Fixed PR #106 - #22 E prover Direct email on Thursday, 2 April 2026 Fixed Commit ebb7430: “Fixed parser source bug … Thanks to Jiangjing Xu”. I have the email. Can we add it here? #23 Zipperposition GitHub Issue #108 Fixed PR #109 - #24 Z3 NA Fixed Old bug in Isabelle-bundled Z3 4.4.0 - #25 Z3 NA Fixed Old bug in Isabelle-bundled Z3 4.4.0 - Finding #9 The fix was done just after the report. We used an LLM (OpenAI, 15/07/2026, GPT 5.5 High configuration) to map each fix to the reported issue: This changeset is **most closely related to Finding #9**, because it modifies `src/Pure/Concurrent/delay.scala` and the way delayed events are scheduled throughout Isabelle. However, **it does not appear to be the direct fix for Finding #9**. Finding #9 concerns an exception escaping from `Delay.run()`, killing the shared event-timer thread. Its proposed fix was to log the exception **without rethrowing it**. In this changeset, the relevant modification is instead: ```scala -if (do_run) event +if (do_run) app(event) ``` It also replaces the global `Delay` factory with `Delay_Ops`, introduces separate `GUI.Delay` and `Resources.Delay` objects, and supplies context-specific loggers and execution mechanisms. The GUI version, for example, sends the event through `GUI_Thread.later`. There is no shown removal of the problematic exception rethrow, and the changeset contains no new `catch` or exception-handling logic. Therefore: > **Classification: related follow-up/refactoring for Finding #9, but not sufficient evidence of the direct Finding #9 fix.** It is clearly not: * **Finding #10**, which concerns `Progress.stopped` consuming and caching a thread-interruption flag. * **Finding #11**, which concerns recursive XML traversal and stack overflow. * **Finding #12**, which concerns null handling in `XML.Output.string`. **Best label:** **Finding #9-related architectural change**, with medium confidence that it was motivated by or followed the Finding #9 discussion, but low confidence that this changeset itself fixes the reported exception-rethrow defect. Finding #12 The fix was done just after the report. We used an LLM (OpenAI, 15/07/2026, GPT 5.5 High configuration) to map each fix to the reported issue: This changeset is fixing **Finding #12 — XML serialisation null-handling corruption**. Finding #12 identifies this exact code in `XML.Output.string`: ```scala if (str == null) { builder ++= str } ``` Because Scala/Java’s `StringBuilder.append(null)` writes the four characters `"null"`, a null value could silently corrupt the serialised XML rather than causing an explicit failure. The changeset removes that special null branch: ```scala str foreach { ... } ``` Consequently, a null string is no longer silently converted into the text `"null"`. Instead, it fails, which reflects the maintainer’s stated position that valid XML trees must never contain null. The additional `Tree.toString` protection returns `"<malformed>"` for applicable XML errors, making top-level diagnostic output more robust. ### Classification > **Changeset `98810e4d19d9` → Finding #12** **Confidence:** Very high — it changes the exact `XML.Output.string` code described in Finding #12. There is a minor difference between the student’s proposed solution and the accepted implementation: * **Student patch:** make the null branch a no-op. * **Accepted approach:** remove permissive null handling and let malformed XML fail, while making `toString` output more defensive. It is **not Finding #11**, because Finding #11 concerns recursive `filter_elements` traversal causing a possible `StackOverflowError`, not null handling. Findings #13 to #18: The maintainer acknowledged that the reported differences are real, but argued that differences between batch build and PIDE should not automatically be treated as software bugs. We therefore classify such reports as false positives only when the observed divergence does not identify a concrete defect or actionable improvement. See msg00019 for further details. Finding #24 was a crash: Based on the trace, these are all test inputs that lead to an EXC_BAD_ACCESS at location 181: ================ mut_02539_230fd4c313 ================ (lldb) target create "/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3" Current executable set to '/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64). (lldb) settings set -- target.run-args "-smt2" "/Users/xujiangjing/smt_fuzz_v2/mutants/mut_02539_230fd4c313.smt2" (lldb) run warning: libobjc.A.dylib is being read from process memory. This indicates that LLDB could not read from the host's in-memory shared cache. This will likely reduce debugging performance. Process 8749 launched: '/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64) Process 8749 stopped * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010108954f) frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 z3`___lldb_unnamed_symbol_100348702: -> 0x1003487b7 <+181>: movsbl (%rax,%r14), %eax 0x1003487bc <+186>: cmpl $-0x1, %eax 0x1003487bf <+189>: je 0x1003487d4 ; <+210> 0x1003487c1 <+191>: testl %eax, %eax Target 0: (z3) stopped. (lldb) bt * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010108954f) * frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 frame #1: 0x0000000100349064 z3`___lldb_unnamed_symbol_100348fec + 120 frame #2: 0x0000000100349a63 z3`___lldb_unnamed_symbol_100349974 + 239 frame #3: 0x000000010034dfd0 z3`___lldb_unnamed_symbol_10034da76 + 1370 frame #4: 0x0000000100332867 z3`___lldb_unnamed_symbol_1003327b6 + 177 frame #5: 0x0000000100339b95 z3`___lldb_unnamed_symbol_100339b08 + 141 frame #6: 0x00000001002de2a2 z3`___lldb_unnamed_symbol_1002dd64e + 3156 frame #7: 0x00000001006ba18d z3`___lldb_unnamed_symbol_1006b9f90 + 509 frame #8: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #9: 0x00000001006bfca1 z3`___lldb_unnamed_symbol_1006bfae4 + 445 frame #10: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #11: 0x00000001006b68a6 z3`___lldb_unnamed_symbol_1006b6860 + 70 frame #12: 0x00000001006b6af1 z3`___lldb_unnamed_symbol_1006b69d0 + 289 frame #13: 0x00000001005d3bb9 z3`___lldb_unnamed_symbol_1005d39ee + 459 frame #14: 0x00000001005d3035 z3`___lldb_unnamed_symbol_1005d2fa4 + 145 frame #15: 0x00000001005d2af1 z3`___lldb_unnamed_symbol_1005d2806 + 747 frame #16: 0x000000010053477b z3`___lldb_unnamed_symbol_100534638 + 323 frame #17: 0x000000010051d453 z3`___lldb_unnamed_symbol_10051cd84 + 1743 frame #18: 0x00000001005234ec z3`___lldb_unnamed_symbol_1005233d0 + 284 frame #19: 0x0000000100510968 z3`___lldb_unnamed_symbol_100510940 + 40 frame #20: 0x000000010000b241 z3`___lldb_unnamed_symbol_10000b110 + 305 frame #21: 0x000000010000ac4e z3`___lldb_unnamed_symbol_10000aa10 + 574 frame #22: 0x0000000100000f74 z3`___lldb_unnamed_symbol_100000f40 + 52 (lldb) quit ================ mut_02606_702c48cda4 ================ (lldb) target create "/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3" Current executable set to '/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64). (lldb) settings set -- target.run-args "-smt2" "/Users/xujiangjing/smt_fuzz_v2/mutants/mut_02606_702c48cda4.smt2" (lldb) run warning: libobjc.A.dylib is being read from process memory. This indicates that LLDB could not read from the host's in-memory shared cache. This will likely reduce debugging performance. WARNING: unknown logic, ignoring set-logic command Process 8821 launched: '/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64) Process 8821 stopped * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010347c7cf) frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 z3`___lldb_unnamed_symbol_100348702: -> 0x1003487b7 <+181>: movsbl (%rax,%r14), %eax 0x1003487bc <+186>: cmpl $-0x1, %eax 0x1003487bf <+189>: je 0x1003487d4 ; <+210> 0x1003487c1 <+191>: testl %eax, %eax Target 0: (z3) stopped. (lldb) bt * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010347c7cf) * frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 frame #1: 0x0000000100349064 z3`___lldb_unnamed_symbol_100348fec + 120 frame #2: 0x0000000100349a63 z3`___lldb_unnamed_symbol_100349974 + 239 frame #3: 0x000000010034dfd0 z3`___lldb_unnamed_symbol_10034da76 + 1370 frame #4: 0x0000000100332867 z3`___lldb_unnamed_symbol_1003327b6 + 177 frame #5: 0x0000000100339b95 z3`___lldb_unnamed_symbol_100339b08 + 141 frame #6: 0x00000001002de2a2 z3`___lldb_unnamed_symbol_1002dd64e + 3156 frame #7: 0x00000001006bfcf5 z3`___lldb_unnamed_symbol_1006bfae4 + 529 frame #8: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #9: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #10: 0x00000001006b68a6 z3`___lldb_unnamed_symbol_1006b6860 + 70 frame #11: 0x00000001006b6af1 z3`___lldb_unnamed_symbol_1006b69d0 + 289 frame #12: 0x00000001005d3bb9 z3`___lldb_unnamed_symbol_1005d39ee + 459 frame #13: 0x00000001005d3035 z3`___lldb_unnamed_symbol_1005d2fa4 + 145 frame #14: 0x00000001005d2af1 z3`___lldb_unnamed_symbol_1005d2806 + 747 frame #15: 0x000000010053477b z3`___lldb_unnamed_symbol_100534638 + 323 frame #16: 0x000000010051d453 z3`___lldb_unnamed_symbol_10051cd84 + 1743 frame #17: 0x00000001005234ec z3`___lldb_unnamed_symbol_1005233d0 + 284 frame #18: 0x0000000100510968 z3`___lldb_unnamed_symbol_100510940 + 40 frame #19: 0x000000010000b241 z3`___lldb_unnamed_symbol_10000b110 + 305 frame #20: 0x000000010000ac4e z3`___lldb_unnamed_symbol_10000aa10 + 574 frame #21: 0x0000000100000f74 z3`___lldb_unnamed_symbol_100000f40 + 52 (lldb) quit Finding #25 was a crash: Based on the trace, these are all test inputs that lead to an EXC_BAD_ACCESS at location 343: ================ mut_04980_25978f85bf ================ (lldb) target create "/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3" Current executable set to '/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64). (lldb) settings set -- target.run-args "-smt2" "/Users/xujiangjing/smt_fuzz_v2/mutants/mut_04980_25978f85bf.smt2" (lldb) run warning: libobjc.A.dylib is being read from process memory. This indicates that LLDB could not read from the host's in-memory shared cache. This will likely reduce debugging performance. Process 8839 launched: '/Users/xujiangjing/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64) Process 8839 stopped * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x6001021b559f) frame #0: 0x000000010034cc2d z3`___lldb_unnamed_symbol_10034cad6 + 343 z3`___lldb_unnamed_symbol_10034cad6: -> 0x10034cc2d <+343>: movsbl (%rcx,%rdx), %ecx 0x10034cc31 <+347>: testl %ecx, %ecx 0x10034cc33 <+349>: je 0x10034cc52 ; <+380> 0x10034cc35 <+351>: cmpl $-0x1, %ecx Target 0: (z3) stopped. (lldb) bt * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x6001021b559f) * frame #0: 0x000000010034cc2d z3`___lldb_unnamed_symbol_10034cad6 + 343 frame #1: 0x000000010034e345 z3`___lldb_unnamed_symbol_10034da76 + 2255 frame #2: 0x0000000100332867 z3`___lldb_unnamed_symbol_1003327b6 + 177 frame #3: 0x0000000100339b95 z3`___lldb_unnamed_symbol_100339b08 + 141 frame #4: 0x00000001002de2a2 z3`___lldb_unnamed_symbol_1002dd64e + 3156 frame #5: 0x00000001006bd840 z3`___lldb_unnamed_symbol_1006bd7de + 98 frame #6: 0x00000001006bfca1 z3`___lldb_unnamed_symbol_1006bfae4 + 445 frame #7: 0x00000001006ba18d z3`___lldb_unnamed_symbol_1006b9f90 + 509 frame #8: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #9: 0x00000001006bfca1 z3`___lldb_unnamed_symbol_1006bfae4 + 445 frame #10: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #11: 0x00000001006b68a6 z3`___lldb_unnamed_symbol_1006b6860 + 70 frame #12: 0x00000001006b6af1 z3`___lldb_unnamed_symbol_1006b69d0 + 289 frame #13: 0x00000001005d3bb9 z3`___lldb_unnamed_symbol_1005d39ee + 459 frame #14: 0x00000001005d3035 z3`___lldb_unnamed_symbol_1005d2fa4 + 145 frame #15: 0x00000001005d2af1 z3`___lldb_unnamed_symbol_1005d2806 + 747 frame #16: 0x000000010053477b z3`___lldb_unnamed_symbol_100534638 + 323 frame #17: 0x000000010051d453 z3`___lldb_unnamed_symbol_10051cd84 + 1743 frame #18: 0x00000001005234ec z3`___lldb_unnamed_symbol_1005233d0 + 284 frame #19: 0x0000000100510968 z3`___lldb_unnamed_symbol_100510940 + 40 frame #20: 0x000000010000b241 z3`___lldb_unnamed_symbol_10000b110 + 305 frame #21: 0x000000010000ac4e z3`___lldb_unnamed_symbol_10000aa10 + 574 frame #22: 0x0000000100000f74 z3`___lldb_unnamed_symbol_100000f40 + 52 (lldb) quit =====