It seems like the Why3 project attempts verification of only "simple" programs without concurrency and higher-order functions. On the other hand, the Iris Project is an attempt to verify higher-order concurrent programs, see e.g. https://iris-project.org/pdfs/2017-case-study-verifying-dart...
Iris is a separation logic, a framework for proving the properties of programs. There are many like it, Iris is just one of the recent examples.
To prove statements in this logic, you have to rely on the proving facilities of the host environment, for instance Coq in your linked example. Most of the proof is then written by hand and quite tedious. The difference is that Why3 attempts to automatise as much of this workload as possible, most frequently with the help of SMT solvers.
With the unexpected result that the here so beloved Z3 solver is actually the worst of all used solvers. You shouldn't blindly use everything with a python binding. https://hal.inria.fr/hal-00967132/en/
Has anyone used this to verify any significant (or insignificant) real world software? Like programs or libraries used in production? How long did it take? How hard was it?
It's mainly used as a backend by stuff like Frama-C and SPARK. They, esp SPARK, do get used in industry. I stay submitting that stuff on Lobste.rs so click the formalmethods tag if interested. Here's a list of Why3 stuff:
