Open source tools for software engineering teams using AI

Automatic generation of formal specification and verification annotations using LLMs and test oracles

João Pascoal Faria and Emanuel Trigo and Vinicius Honorato and Rui Abreu misc 2026 Source: z-spec

Note

LLMs generate correct Dafny annotations for 98.2% of programs within 8 repair iterations using verifier feedback.

faria2026dafny