The LEGO Proof Assistant
A powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs.