You mentioned good tools available for Z - do you have any recommendations? I have tried in the past using VDM (alternative to Z, similar level) for writing down specifications precisely, but could never find adequate tools for maintaining/checking proofs/derivations.