Really neat project. Thanks for sharing.
One thing I'm always skeptical about with these formal verification projects is their ability to continue delivering useful results over time. Once somebody submits a patch to binary_search the analysis you've done will be invalidated. Have you put any thought into how a test suite of formal verifications might be maintained over time? Is this something we could add to Rust's CI so that we know binary_search is correct for all time?