VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education
摘要
Developing highly reliable software requires the use of formal verification methods, but integrating them into the education of IT students is difficult due to the gap between theoretical understanding and practical skills. In this paper, we present the design, implementation, and analysis of VeHa-2025, a national verification hackathon aimed at overcoming these challenges through hands-on learning, particularly through competitions focused on specific verification problems. Our event combines tracks in model checking (SPIN, TLA+) and deductive verification (Isabelle/HOL, Coq-Rocq, Why3, C-lightVer). Launched in 2023 as a volunteer initiative by a group of academics, VeHa evolved into an academy-industry partnership by 2025. VeHa-2025 included a structured educational cycle consisting of preparatory workshops, an invited lecture, a three-day competitive problem-solving period, and a post-event verification of solutions. The analysis of metrics, submitted solutions, and participant feedback presented in this article demonstrates the growing effectiveness of our hackathon in developing practical skills, building a community, and equipping participants with competencies in formal methods that are in demand in industry. We argue that such competitive, practice-oriented formats are a valuable pedagogical tool for motivating and training the next generation of software verification engineers.