I don't understand these comments, you have no idea what F* provides for this project to work, but yet you can somehow perceive that rust would be a good language for this project. Really?
Rust is a cool language for safe low-level programming with concurrency, but it is not targeted at program verification. F* can also do safe low-level programming by extraction to C, while also verifying that the code is functionally correct and secure. That's of course a lot more work, but also a lot stronger than the kind of guarantees one can get informally in rust (e.g. memory safety).
F* is significantly more hardcore than Rust. Dependent types, refinement types, and effects are powerful features it has that Rust doesn't. I do a bit of Rust myself, but the world would probably be better if Rust was only a stepping stone toward languages like F*, Idris, ATS and friends. :)