Competition Rules
This page describes how the Verified Software Competition is structured: the timeline of a typical edition, what participants are expected to submit, and the criteria used to evaluate solutions. Details have evolved across editions, but the core framework remains consistent.
How an Edition Unfolds
Each VSComp edition follows a broadly similar timeline, though the exact dates and durations vary. Understanding this structure helps participants plan their effort and reviewers set expectations. The typical sequence is as follows.
Announcement & Problem Release
The organising committee announces the competition and publishes the problem set. Each problem includes a natural- language description, a formal or semi-formal specification of the expected behaviour, and any constraints on the solution format. Participants may begin working immediately.
Submission Window
A defined period during which participants develop and submit their solutions. The window has typically ranged from several days to a few weeks, depending on the edition. During this period, the organisers may publish clarifications or errata if ambiguities are discovered in the problem statements. Participants are free to use any verification tool or proof assistant.
Review & Evaluation
After the submission window closes, the organising committee reviews all submissions against the published evaluation criteria. This phase involves checking that proofs are mechanically valid, assessing the completeness of each solution, and evaluating the clarity of the verification approach.
Results & Publication
Results are announced and, where applicable, published in workshop proceedings or technical reports. Some editions have been associated with formal-methods workshops or conferences, providing a venue for participants to present and discuss their solutions. The publications page lists documented reports from past editions.
Not every edition has followed this template exactly. The 2010 edition, for example, used a somewhat compressed timeline as a pilot. Later editions refined the process, adding explicit clarification periods and more structured evaluation rubrics. The years index provides edition-specific details.
What Participants Submit
A VSComp submission is expected to include, at minimum, the following components:
- Implementation: Source code that solves the stated problem. This may be in any programming language supported by the participant's chosen verification tool.
- Specification: A formal description of the properties that the implementation is claimed to satisfy. This includes preconditions, postconditions, invariants, and any relevant auxiliary definitions.
- Proof: A machine-checkable proof that the implementation meets the specification. The proof must be verifiable by running the appropriate tool — manual or paper-only arguments do not qualify.
- Documentation: A brief written explanation of the verification strategy. This is not a formal requirement in all editions but has been increasingly emphasised since 2014.
The competition does not restrict the choice of tool. Participants have used a wide range of systems, including Dafny, Why3, Frama-C, Coq, Isabelle/HOL, Lean, SPARK, KeYmaera X, TLA+, Event-B, and others. What matters is that the proof is mechanically checkable — the organising committee must be able to reproduce the verification result. Practical guidance on reproducibility is discussed on the solutions page.
How Solutions Are Evaluated
Solutions are assessed along three main dimensions. These categories have been consistent across editions, though the specific rubric and relative weighting have been refined over time.
Does the proof actually establish the specified properties? This is the most fundamental criterion. A solution is correct if the stated specification captures the intended behaviour and the proof is mechanically valid. Reviewers check that there are no unchecked assumptions, admitted lemmas, or trusted axioms that undermine the proof's soundness.
Does the solution address the full scope of the problem, or only a subset? A solution that proves sorting correctness but omits the permutation property, for instance, would score lower on completeness than one that addresses both. Partial solutions are accepted but noted as such.
Is the proof structured in a way that a knowledgeable reader can follow? Clarity includes the organisation of the proof script, the naming of lemmas and invariants, and the quality of any accompanying documentation. A clear solution helps others learn from the approach.
These three criteria are intentionally broad. The organisers have generally avoided prescribing a rigid scoring formula, preferring instead to exercise expert judgement informed by the criteria. This reflects the reality that formal verification solutions are difficult to compare on a single numerical scale — a concurrency proof and a compiler-correctness proof involve fundamentally different techniques, and evaluating them requires domain-specific expertise.
Competition Format in Detail
VSComp is an online competition. There is no physical venue; participants work remotely and submit their solutions electronically. This format was chosen deliberately to maximise accessibility. Formal verification is a global research community, and an online format removes geographic barriers to participation.
Each edition typically publishes five problems, though the exact number has varied. Problems are released simultaneously at the start of the submission window. Participants may attempt any or all problems — there is no requirement to solve every challenge. Partial solutions (addressing a subset of a problem's requirements) are accepted and evaluated on the criteria described above, with completeness scored accordingly.
The submission mechanism has varied between editions. In some years, solutions were submitted via email; in others, a web-based submission system was used. The specific mechanism is documented on each year's hub page. Regardless of the mechanism, all submissions are expected to include the artifacts listed in the submission expectations section above.
Who Can Participate
VSComp is open to anyone with an interest in formal software verification. Participants have included university research groups, individual researchers, graduate students, and industry practitioners. Teams are permitted, and there is no restriction on team size, though each submission is evaluated as a single entry.
There are no entry fees, and participation does not require institutional affiliation. The competition's purpose is to advance the state of the art in verified software, and broad participation serves that goal. That said, the problems are designed for participants with genuine expertise in formal methods — they are not introductory exercises.
Questions about eligibility or format are addressed in the frequently asked questions section.
Changes Across Editions
The rules described on this page represent the general framework that has been consistent across all editions. However, specific details have changed. The 2010 edition, as the pilot, had fewer formal requirements for documentation. By 2014, the organisers added an explicit expectation for written explanations of the verification strategy. The 2015 and 2017 editions placed greater emphasis on completeness, reflecting the community's recognition that partial proofs — while valuable — should be clearly distinguished from complete ones.
For edition-specific rule variations, consult the relevant year hub page. The problems catalogue notes any problem-specific requirements that go beyond the general rules.
Browse the full problem catalogue to see what participants are asked to verify, organised by year, domain, and difficulty.
The solutions archive shows how participants have approached these challenges, with notes on tools, techniques, and reproducibility.
Common questions about the competition format, eligibility, and submission process are answered on the FAQ page.
Visit the years index for a timeline of every edition with links to year-specific hubs.