How Amazon Web Services Uses Formal Methods is in this month's Communications of the ACM. This version isn't changed much from the versions that have been online for a few months, but it's great to see it get some more attention.
In the same issue of CACM is Leslie Lamport's Who Builds a House without Drawing Blueprints?. Fans of his writing won't find anything new in there, but it's a perspective and opinion that I love to see gain more traction.
We think in order to understand what we are doing. If we understand something, we can explain it clearly in writing. If we have not explained it in writing, then we do not know if we really understand it.
And the conclusion:
Thinking does not guarantee that you will not make mistakes. But not thinking guarantees that you will.
It's a very good take on the subject. As our experiences at Amazon have shown, specification can be an extremely powerful tool in the system designer's and programmer's toolbox. It's even more useful as a team member, where the ability to communicate particularly tough ideas formally and concisely really helps collaboration.
Other good formal methods reading this week: