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. We present a fuzzing-based approach for testing Isabelle by targeting components that are interacting with its trusted core. Four students investigated different subsystems over six months, uncovering 24 distinct anomalies. We reported 16 findings to developers, of which 11 were confirmed. We further wrote 10 patches, resulting in 6 accepted pull requests, thus improving the quality of the wider 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 #1--5 Poly/ML Lexer (x86) Enzo Bestetti #6--8 Poly/ML ARM64 Aravinth Kaneshalingam #9--19 Isabelle/jEdit Bartosz Gowacki #20--24 Sledgehammer Jiangjing Xu 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) 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 D. Matthews, polyml@lists.polyml.org, 19 Mar 2026 [link] Enzo, Mohammad, was it fixed? #2 Poly/ML lexer X86 GitHub Issue #256 Fixed Commit fc87489 - #3 Poly/ML lexer X86 GitHub Issue #258 Fixed Commit 2a1c2ab - #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 Enzo, can we have this email and check with David if this is okay to add here? #5 Poly/ML lexer X86 N/A Not reported Informational observation; likely intentional parser deviation Enzo, did we report it? Discussed it with anyone? #6 Poly/ML ARM64 GitHub Issue #271 Reported - #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 Fixed Maintainers committed a patch in response to our report that prevents the observed behaviour from happening - #10 Isabelle/jEdit Development branch Fixed Maintainers committed a patch in response to our report that prevents the observed behaviour from happening - #11 Isabelle/jEdit Mailing list Acknowledged; patch submitted Patch submitted to developers Bartosz, Mohammad: Need to get more evidence #12 Isabelle/jEdit Mailing list 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 Fixed PR #103 - #21 Zipperposition GitHub Issue #104 Fixed PR #106 - #22 E prover Direct + mailing list Fixed Commit ebb7430: “Fixed parser source bug … Thanks to Jiangjing Xu” Jiangjing, do we have the email? #23 Zipperposition GitHub Issue #108 Fixed PR #109 - #24 Z3 NA Fixed Old bug in sabelle-bundled Z3 4.4.0 - #25 Z3 NA Fixed Old bug in sabelle-bundled Z3 4.4.0 - Bug #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 : movsbl (%rax,%r14), %eax 0x1003487bc : cmpl $-0x1, %eax 0x1003487bf : je 0x1003487d4 ; 0x1003487c1 : 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 : movsbl (%rax,%r14), %eax 0x1003487bc : cmpl $-0x1, %eax 0x1003487bf : je 0x1003487d4 ; 0x1003487c1 : 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 Bug #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 : movsbl (%rcx,%rdx), %ecx 0x10034cc31 : testl %ecx, %ecx 0x10034cc33 : je 0x10034cc52 ; 0x10034cc35 : 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 =====