Comment by kolinko

Of course, and correct verification assumptions were always a challenge, and they are a possible failure point - but 95%(?) of labour was then proving the code, and now that part can be largely automated.

Speaking of how difficult can it be to write a proper spec, I think a few years ago someone found a bug in spec in a helloworld-like example in a book about formal methods, and a bug in the code.