Question About Suitable Verification Challenges for a Beginner

[Fengolo]

Hi Verify Rust maintainers,

I'm an undergraduate computer science student pursuing my bachelor's degree, and I'm interested in contributing to the Verify Rust Std Lib project.

I'd like to take on a verification challenge that is appropriate for my current level while still allowing me to learn and make a meaningful contribution. I have experience with C memory management, but I'm still new to Rust, having only recently discovered the language. I've found it really interesting so far, and I'm particularly interested in formal verification, which I'm currently studying in a university course. In fact, I'd like to explore formal verification tools for Rust as a possible topic for my bachelor's thesis.

With this in mind, I'd be interested to learn more about the learning curve for the tools involved in these challenges, such as Kani, and which challenges might be suitable for me once I've gained a better understanding of Rust and the relevant tools. I'd also appreciate your perspective on how much time I might need to invest before becoming proficient enough with these tools to make a meaningful contribution to the project.

Could you recommend how I should assess the difficulty of the open challenges, or suggest which ones might be a reasonable starting point for an undergraduate contributor?

I'm happy to spend time understanding the relevant code, learning the verification tools, and working through the challenge requirements before getting started.

Thank you for your time and for maintaining this project!