This artifact provides a complete Runtime Error Guided Specification Generation system using Large Language Models. Package Contents: 1. Docker image with complete verification system (Frama-C + LLM integration) 2. Lightweight benchmark suite (51 test cases from new-frama-c-problems) 3. Large-scale benchmark suites (Atomthreads RTOS, Contiki-OS, X.509 parser) 4. pre-generated annotated results for all benchmarks 5. Complete execution logs with detailed verification statistics 6. Easy-to-use runner script (docker-run.sh) Users can: - View pre-generated annotated C files with formal specifications instantly - Reproduce experiments by re-running verification (~17-19 hours total) - Examine detailed logs showing node/assertion-level verification results - Extend the system with custom C programs Experiment Suites: - Benchmark: 51 test cases (~60-70 min) - Atomthreads: RTOS kernel (~13-14 hours) - Contiki: IoT operating system (~60-70 min) - X509: Parser verification (~2.5 hours) For detailed instructions and experimental methodology, please refer to the RTE-SPEC-GEN-README.md