The style guidelines below have been developed for the proof websites generated by Kumo, with the aim of making proofs much easier to understand than is usual. To clarify the discussion, we distinguish between abstract proofwebs and display proofwebs; the first contains only proof information, while the second also includes display information. We will use the word unit for any block of information of the same kind within a display proofweb.

1. A homepage is provided for each major proof part; these serve to introduce and motivate the problem to be solved and the approach taken to the solution.
2. Tatami pages are the basic constituents of display proofwebs; each tatami page has one or more proof units showing its inference rule applications, interleaved with one or more explanation units; it is feasible to have both on the same web page because there should only be a small number of proof steps per page (about 7 non-automatic rules works well). Tatami pages are also called "proof pages."
3. The explanation units of tatami pages are prover-supplied informal discussions of proof concepts, strategies, obstacles, etc.; these may contain graphics, applets, and of course text.
4. Tatami pages can be browsed in an order designed by the prover to be helpful and interesting to the reader; if possible, these pages should tell a story about how obstacles were overcome (or still remain); this order will be called the narrative order. (See Notes on Narrative for more information on the theory of narrative used here.)
5. Major proof parts, including lemmas, have their own subwebsites, each with the same structure as the main proof, including homepage and explanation units. These appear in a separate dedicated persistent popup window.
6. Tatami pages also have associated formal proof scores, which appear in another separate popup window when summoned from a tatami page. It is convenient to have a separate window because users usually want to look at the proof and explanation at the same time as the proof score. Readers can also request proof score execution, and the result is then displayed in the same window as the score, so that one can easily alternate between them. (The proof score is sent to an OBJ server and the result is returned for display.)
7. Major proof parts can have an optional closing page, to sum up important results and lessons; these appear in the same window as their tatami pages.
8. Formal proof steps are automatically linked to pre-existing tutorial background pages; e.g., each application of induction is linked to a webpage that explains the kind of induction used. Tutorial pages have their own dedicated persistent popup window.
9. A menu of open subgoals appears on each homepage, and error messages are placed on appropriate pages. In database mode, a summary of this information may be seen in the status window, which is a specialized popup that reports any currently open subgoals.