A system for converting a natural language specification document into a formal specification would be interesting.