Formal Specs Inferred From Tests Alone, Without White-Box Access to the Implementation

arXiv 2608.13240·low signalXBlueskyLinkedInCopy link

Prior LLM specification-inference work reads the source code, which blocks industrial adoption on IP-risk and deployment-cost grounds. This approach shows the LLM only the program interface, selected inputs and the resulting outputs or state changes drawn from test code and dynamic execution traces, then validates candidate JML specifications with bounded model checking and iterates on the feedback. Initial results on SpecGenBench suggest tests can guide LLMs to meaningful specifications, while flagging checker compatibility and the quality of diagnostic feedback as the limiting factors for reliable refinement — early-stage work, single-source, but a genuinely different threat model for spec synthesis.