Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles

João Pascoal Faria, Emanuel Trigo, Vinicius Honorato +1

Recent verification tools aim to make formal verification more accessible to software engineers by automating most of the verification process. However, annotating conventional pro…