New target: Isabelle parser fuzzing via JVM (Jazzer)

[quinn-dougherty]

Background

From the 2026-06-22 evals team meeting: the Isabelle theorem prover's parser is written in Scala (JVM), has no OSS-Fuzz coverage, and is a high-value target — it processes untrusted .thy files in a security-sensitive context. The team decided to fuzz it by generating malformed Isabelle theory files and using JVM fuzzing infrastructure.

Approach

• Corpus: malformed .thy theory files. Isabelle's grammar is well-documented; generate structurally valid but semantically broken inputs (bad term syntax, unclosed theory/end blocks, unicode edge cases, deeply nested expressions).
• Fuzzer: Jazzer — libfuzzer-compatible JVM fuzzer. If Jazzer integration is painful, a thin C shim that shells out to java is an acceptable fallback.
• Docker image: extend OSS-Fuzz base or use a JVM-capable base; include isabelle binary or build from source.

Scope

• Docker target in targets/isabelle/
• Corpus of ~20 seed .thy files (valid and boundary-case)
• Jazzer harness targeting the Isabelle theory parser entry point
• Confirm harness actually exercises parsing (not a stub)
• metadata.yaml

Open questions

• Which Isabelle version to pin (stable release vs. nightly)?
• Is the Scala source accessible enough to identify the parser entry point, or do we black-box it?
• Jazzer vs. java-fuzzer: decide before starting build work.