Can't wait for CBMC and Why3 connection efforts for rust to start being used by AWS and their formal methods people (I know they're into TLA+ and I wish there w

Can't wait for CBMC and Why3 connection efforts for rust to start being used by AWS and their formal methods people (I know they're into TLA+ and I wish there was also some work going on to connect rust/SPARK and temporal logic tools better too).