Challenge XXXX1: Challenge Title

  • Status: One of the following: [Open | Resolved | Expired]
  • Solution: Option field to point to the PR that solved this challenge.
  • Tracking Issue: Link to issue
  • Start date: YY/MM/DD
  • End date: YY/MM/DD

Goal

Describe the goal of this challenge with 1-2 sentences.

Motivation

Explain why this is a challenge that should be prioritized. Consider using a motivating example.

Description

Describe the challenge in more details.

Assumptions

Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".

Success Criteria

Here are some examples of possible criteria:

All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:

FunctionLocation
abcdef

At least N of the following usages were proven safe:

FunctionLocation
xyz123

All proofs must automatically ensure the absence of the following undefined behaviors ref:

List of UBs

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

1

The number of the challenge sorted by publication date.