I don't necessarily disagree with your points here, but for completeness you should note that DO-178B has been moving to DO-178C for a few years now, which incl

I don't necessarily disagree with your points here, but for completeness you should note that DO-178B has been moving to DO-178C for a few years now, which includes references to formal methods for systems verification, specifically DO-333. Also, that paper by Denney is 10 years old, and some strides have been made since then to improve formal method tools for viable verification.