How Amazon Web Services Uses Formal Methods http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext 読んだ。 AmazonでDynamoDBのローンチ時に、TLA+ http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html によるモデリングとモデル検査を使いだして、設計の検証に用いることで(他の手法では見つけられなかったような)捉えにくいが深刻なバグを発見できたり、バグ修正が正しい修正であることを検証したり、アグレッシブな性能上の最適化をする際に正当性が損なわれないことを確かめたりとかに使って、良かったよという話。

以下は Key insights として書かれているポイント。
* Formal methods find bugs in system designs that cannot be found through any other technique we know of.
* Formal methods are surprisingly feasible for mainstream software development and give  good return on investment.
* At Amazon, formal methods are routinely applied to the design of complex real-world software, including public cloud services.

その他、個人的に面白かった箇所の抜粋:

* In industry, formal methods have a reputation for requiring a huge amount of training and effort to verify a tiny piece of relatively straightforward code, so the return on investment is justified only in safety-critical domains (such as medical systems and avionics). Our experience with TLA+ shows this perception to be wrong.

* We find this rigorous “what needs to go right” approach to be significantly less error prone than the ad hoc “what might go wrong” approach.

* We also find that writing a formal specification pays dividends over the lifetime of the system.

* A precise, test able description of a system becomes a what-if tool for designs, analogous to how spreadsheets are a what-if tool for financial models. なんだかAlloy的なことを言っているなぁ、と思っていたら、後からAlloyの話も出てきて、Alloyも試したけれど、表現能力的な面で結局TLA+にしたとのことだった。

* He believes the investment he made in writing and checking the formal TLA+ specifications was more reliable and less time consuming than the work he put into writing and checking his informal proofs.

あと、DynamoDBの設計のモデル検査では、分散版のTLA+を使って、10台のcc1.4xlargeインスタンス(8コア+ハイパースレッディングとRAM23GB)のクラスタでやったとのこと。モデル検査もクラスタで実行する時代なんやなぁ。