That&#x27;s quite possible, and most proof of correctness systems can do it, but there&#x27;s no syntax in Rust for talking about the necessary object invariants.<p>Object invariants are assertions which must be true whenever control is not within the object. The object invariants must be true when control leaves the object by exiting any public function.  Nothing outside the object must be able to alter the variables involved in the object invariant. Only one execution thread can be in the object at a time.
If you can demonstrate all of those conditions, assuming the invariant is true at entry to the object, you have proved the object invariant.<p>This is a useful and well-understood concept in the proof world, but isn&#x27;t seen much in programming languages.