I confirm that we're following closely what Xavier is doing for Rust, and even copied his work on "prophecy variables" to take the effects of borrowing into account in loop invariants in SPARK!
Your plans for having Rust analyzers collaborate look very cool! Like you said, the first challenge is to agree on a base specification language. I hope this gets discussed at the next Rust Verification Workshop.
Your plans for having Rust analyzers collaborate look very cool! Like you said, the first challenge is to agree on a base specification language. I hope this gets discussed at the next Rust Verification Workshop.