Lol. If that were true software would've been a lot better historically... Model checkers don't scale to 90% of the software we write. Typically you have to 1) heavily abstract the program and 2) put it in some sort of harness to specify how you want to model the outside world (which will always fall short of practice). And probably 10 other workarounds since most model checkers are Research Grade Software™. Not saying they're not tremendously useful, but that bullet doesn't hold up at all.

Too bad the github readme doesn't explain how the choreographic side of Wyzer works, or even what it looks like (please correct me if I'm wrong, couldn't find it after a quick skim).