The book Out of Their Minds quotes Leslie Lamport on proofs:
The proofs have been carried out to an excruciating level of detail … The reader may feel that we have given long, tedious proofs of obvious assertions. However, what he has not seen are the many equally obvious assertions that we discovered to be wrong only by trying to write similarly long, tedious proofs.
See Lamport’s paper How to Write a Proof. See also Complementary validation.
An essential aspect of Lamport’s idea is a tree structure for the presentation of proofs, so that you start with a high level description and you can drill down to deeper and deeper levels of detail as needed for conviction. This is to be supported by software.
It seems to me that good expositors do this even without software support.