You might be overthinking this. What you want is a cost-effective way of reaching the correctness you need; i.e. a good bug-found-per-hour rate. Unless you have

You might be overthinking this. What you want is a cost-effective way of reaching the correctness you need; i.e. a good bug-found-per-hour rate. Unless you have a lot (years) of experience writing formal proofs, I suggest you try them, first. They generally do not have a good correctness ROI compared to other methods. But nothing and no one can give you an answer without knowing the particulars of your project, the people working on it, and the correctness goals. You'll have to try a few things for a bit and then make up your mind. Just remember that 1. the smaller your project is and the fewer people working on it the less the particular formal method chosen matters, and 2. in formal methods, going from 99.999% correct to 99.9999999% correct can be a 10x factor in cost, so the assumption that more correct = better is generally wrong as there are diminishing returns. Of course, if you just want to do this to learn about formal methods rather than find one that you can frequently use in large projects, then the choice matters even less. In terms of basic principles, the tools you mentioned are much closer to one another than they are different.