The difference is that Rust and Java can only verify certain properties. I can build model checks to verify any property that I can discharge with an SMT solver

The difference is that Rust and Java can only verify certain properties. I can build model checks to verify any property that I can discharge with an SMT solver, which is significantly more powerful. For instance, I can build function contracts that verify that if a function succeeds, it performs certain actions, and if it fails, it does not. I can verify that a function properly manages external resources, performs authorization checks, or always follows data structure invariants. I don't need to build full formal specifications to do this. I can verify just the subset that is important. I can do more than what Rust or Java provides. I can add more rules that must be followed, or in cases where it doesn't matter, I can relax specific rules without reaching for clumsy annotations like "unsafe", or using an FFI.