Oh, that takes me back to 1982.[1] This is very similar to what we did back then. The syntactical approach is almost identical. It's much more programmer-friendly than some other approaches. One of the problems with proof of correctness is that the people doing it tend to fall in love with the formalism, and it all becomes too abstract and hard. This project didn't do that.

It's not clear what they do when they need to prove something beyond what an SMT solver can do. That's supposed to be covered in section 11.4, "forall and exists: writing and using triggers, inline functions". What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)

That's the right approach - use an SMT solver for the easy stuff, which should be 90-95% of the proofs. Then use something else for the hard stuff. We used the Boyer-Moore prover, a predecessor to the ACL system. Others have used proof-checkers, and Lean. There's recent interest in using LLMs to drive something like Lean; the LLMs make mistakes but the proof checker catches them. Looks like they haven't gotten to this part yet.

The way to partition the problem is to use two "assert" statements in succession. An assert statement is a proof goal before the assert, and is assumed true after the assert. So when you hit something hard, you try to bracket it with

    assert(a);
    assert(b);

and get everything to verify with the SAT solver except

    a implies b

Now you have a self-contained expression to prove by some external means. Often you can prove such statements in a generic form, and reuse the proofs.

There should be object invariants, except that Rust doesn't have objects. It does have structs with associated functions and encapsulation. You need some way to express that structs with internal state are consistent before and after being called. C++ has about the right amount of hiding ("abstraction") for this, with public and private fields and functions for objects. Rust's idea of "private" means "same module", not "same struct". So invariants would apply to a module. Then you have to be very organized about when control enters and leaves the module. Like not calling pub functions from inside the module, because the module invariants may not be valid at internal entry to a pub function.

The extensional equality thing is interesting. It needs more description. The basic problem is this: for some types, such as sets, hash tables, and such, objects are supposed to be considered equal if you can't tell from the outside that they're different internally. Formally, the type must have the property

    for all functions f where x is an element of T, 
        x == y implies f(x) == f(y)

That has to be proven for all functions which accept T. Then you can treat type values as equal even if their internal representation is different. Such types can't have any access functions or pub variables which allow you to examine the internal state. For example, if you convert a set to a vector, it has to be sorted, so that you can't tell what the internal order was.

Nice work. Keep plugging.

[1] https://animats.com/papers/verifier/verifiermanual.pdf

Verus is a tool for verifying the correctness of code written in Rust