The KeYmaera X web UI allows you to view a completed proof. After finishing a proof, click on the “Browse Proof” button in the top right-hand corner of the user interface:

How to view a completed proof in KeYmaera X
Fig. 1 - How to view a completed proof in KeYmaera X

The proof browsing interface allows you to expand the proof from the bottom up. Therefore, when the viewer launches, you will see a single sequent with the profen property and an “Expand Details” button on the top of the horizontal line:

Use the Expand Details button to dig into the proof
Fig. 2 - Use the "Expand Details" link to dig into the proof's details

The proof browser shows each step in the proof at the same granularity that was used when constructing the proof. Therefore, you cannot step into automated tactics. If the “auto” tactic is used then you will only be able to see that you ran “auto” and the proof completed; you won’t be able to step into the individual proof steps executed by “auto”.

If the proof branches, then clicking the “Expand Details” link might result in multiple tabs. Just like in the proving interface, each tab corresponds to a branch of the proof:

Use the Expand Details button to dig into the proof
Fig. 3 - The "Expand Details" link results in multiple tabs whenever the proof brances.

The proof displayed by the proof viewer corresponds exactly to an underlying Bellerophon proof script. The proof script can be downloaded by going to the “proofs” page and clicking the file box dialog next to the relevant model:

Downloading the Bellerophon proof script
Fig. 4 - Downloading the Bellerophon proof script.

Thanks to Miguel Velasquez for noticing that this feature was not properly documented and asking for details on the KeYmaera X mailing list. If you have any questions about KeYmaera X, please don’t hesitate to email me (kyxhelp@nfulton.org) or the Keymaera X mailing list.