Rigorous Verification, Open Challenges
VSComp is a periodic online competition that invites researchers and practitioners to solve precisely specified software verification problems. Since 2010, participants have applied deductive verification, model checking, and automated reasoning to demonstrate that their implementations meet formal specifications — from sorting algorithms to concurrent data structures and protocol verification.
Here you will find the competition archive: problem sets, submitted solutions, published reports, and practical guidance on what it takes to produce verified software under competition conditions.
Jump to a Competition Year
VSComp has run in several editions since the inaugural 2010 round. Each year introduces new challenge problems that test different aspects of formal verification — from functional correctness to termination and concurrency. Select a year below to explore its problems, solutions, and supporting materials.
How the Competition Works
Each VSComp round presents a set of challenge problems, each with a precise specification. Participants choose a verification tool — Dafny, Why3, Frama-C, KeY, SPARK, or others — and develop solutions that demonstrably meet the specification. This usually means writing an implementation together with annotations (preconditions, postconditions, loop invariants, ghost state) sufficient for the tool to discharge all proof obligations.
Solutions are evaluated on correctness, completeness of the verification, and clarity of the approach. A competition round typically opens a submission window of one to several days, though the exact format has varied across years. For a detailed breakdown of the evaluation criteria, see the Rules page.
A typical submission includes source code annotated with formal specifications, a description of the verification approach, the tool output showing discharged proof obligations, and sometimes a brief write-up discussing design decisions and any assumptions made.
Browse the Competition Archive
The archive contains problem descriptions, submitted solutions, and (where available) published reports on each competition round. These materials are useful for anyone studying formal verification techniques in practice.
Problems
Challenge specifications spanning topics like sorting, tree operations, concurrency primitives, and protocol verification.
Browse problems →Solutions
Verified implementations from competition participants, organised by year and challenge, with tool and approach details.
Browse solutions →Publications
Published reports and technical papers arising from competition results and methodology discussions.
Browse publications →Recent Updates
The site is periodically updated with corrected materials, newly digitised artifacts, and editorial notes. See the full changelog for a complete history of updates to this archive.
| Date | Update |
|---|---|
| Jan 2026 | Refreshed site structure and navigation; verified all internal links. |
| Sep 2024 | Added detailed problem domain tags and difficulty estimates across all years. |
| Mar 2023 | Consolidated publication records; added citation guidance for solutions. |
| Nov 2021 | Corrected errata in 2014 problem specifications; updated artifact links. |
A Community Effort in Verified Software
The Verified Software Competition grew out of the broader Verified Software Initiative, which brings together researchers working on the grand challenge of producing software that is correct by construction. VSComp provides a concrete, practical forum: here, ideas about specification, proof automation, and tool support are tested against real problems under time constraints.
Whether you are new to formal verification or a seasoned practitioner, the competition archive offers a structured set of benchmark problems and real-world solutions to learn from. For background on the field, see our page on formal verification. For the competition's history across editions, visit the history page.
