A lot of the suggestions so far have really been for CS, not software engineering.

For software engineering, how about a practical way to do proofs of correctness for large real-world systems written in mainstream languages?