The proofs presented in this paper are necessarily informal, but the structured calculational proof format can also be used to present completely formal proofs. It should be noted that for such proofs the format is just that, a format, not a new method of proof. There is a straight-forward translation between the structured calculational format and natural deduction. The existence of the translation, described elsewhere (Grundy to appear), establishes the soundness of structured calculational proof. (The article referenced presents structured calculational proof using an alternative notation, called window inference, which is better suited for interactive use with a mechanised reasoning tool.)
It has also been shown (Grundy to appear), by induction over the structure of natural deduction proofs, that every result that can be established using natural deduction can also be established by structured calculation. This amounts to a completeness result for those logics where natural deduction is complete, and a kind of `relative completeness' for other logics.