In 1995, Leslie Lamport published an essay in the American Mathematical Monthly titled "How to write a proof". In the essay, Lamport introduced the concept of a structured proof, in which the traditional high-level proof is augmented by a sequence of lower levels. Each level of proof expands each step of the higher level into substeps. The amount of detail at the lowest level is rather extreme -- Lamport's proof of the irrationality of the square root of 2 runs to 1.5 pages.
The essay has over 250 citations according to Google Scholar, but I have never seen a proof published in this format. In a PDF or on paper, the extreme detail could be overwhelming; but I think modern web publishing platforms could accommodate it very well (with hierarchical collapsible subsections for each part of the proof).
In any case, are there examples of proofs published in the format suggested by Lamport?