Here is a paper by the AWS team that describes their approach to formal methods and which you could find 'tangible' : http://research.microsoft.com/en-us/um/people/lamport/tla/fo...