This is a small, quick and dirty patch for the KeY prover (1.4.0), overriding the default (useless) LaTeX export mode.
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.