Presenting semi-formal proofs in LaTeX

I've done some reading about presenting somewhat formal proofs (a bit shy of those that can be machine checked), and wanted LaTeX packages that could help me with it. In particular, tedious programming language proofs by near-trivial induction over syntactic structures. I didn't find anything great, but I did find some packages.