Yeah, I guess we can say it works type-wise. 
Yep, in the world of formal verification it’s accepted that at some point one has to trust someone, otherwise one must prove specs ending up with a hierarchy of proofs. It’s not a panacea but at least it’s defined what “works” means so one can reason about it. Without a spec, a program neither works nor doesn’t work, IMHO.