AutoJML: Generation and Verification of JML Specifications Using LLM Agents

Formal specifications such as Java Modeling Language (JML) are essential for program verification, but are complex and error-prone to write manually. Although recent large language model (LLM) based approaches automate specification generation, they often struggle with complex control flow and semantic completeness. We present AutoJML, an LLM agent that generates and refines JML specifications using iterative verification and mutation-based feedback. Evaluated on Java programs with diverse control flow patterns, AutoJML verifies more programs than a state-of-the-art baseline, particularly for multipath and nested loop programs.