Well, for some definition of formal, both state machines and rigorously defined {interfaces|message sequences|protocols} (ie. those with specification-based, generative implementations of endpoints, validating middleware proxies, etc.).

There are two models of reality that I find to be the most useful ones, especially when writing programs. The first is functions, and the second is sequences of states. - Leslie Lamport

... via http://github.com/globalcitizen/taoup