Maude is a good one, too. The K Framework people built on Maude. Then, they built the formal semantics of C on it which they use to prove absence of specific errors. Shows how practically useful these things can be.