Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles. - João Pascoal Faria; Emanuel Trigo; Vinicius Honorato; Rui Abreu 001 (CoRR, 2026)