Testing the Verifier: Automated Testing for Isabelle (Artifact, Working Paper)

Le résumé fourni par la source

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 in Response to our Report Fixed Before We Reported WON'T FIX Not Report Duplicated Poly/ML lexer 1 1 3 0 2 1 1 Isabelle/jEdit 0 0 2 1 7 1 0 Sledgehammer 0 0 4 2 0 0 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

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.