This talk describes some recent work on specifying safety, performance and fault-tolerance properties for some practical network services. It describes the techniques that were used, the accomplishments, the benefits, the drawbacks, and what remains to be done. Examples include TCP and T/TCP, various group communication services, and some toy examples. A theme that recurs throughout the talk is the need for practical, modular, non-probabilistic techniques for performance and fault-tolerance analysis.