KeY now exports nicely formatted logic proofs, using the nifty
The proofs are annotated by rule names and, when relevant, variable instantiations.
Here is an automatically generated proof tree (edit: I noticed the branches appear in the wrong order; this has been corrected):
Instructions: replace existing ProofSaverLatex.java file in /key-1.4.0/system/de/uka/ilkd/key/proof. Recompile. To export in LaTeX mode, just save proof with .tex extension. Insert resulting TeX file in your document, which must use the package bussproofs.