Did you consider using an established Rust verification toolchain like Aeneas?

Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?