diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index d8ef7f4..f6a7d06 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -3951,6 +3951,41 @@ including both a functional correctness theorem as well as a
 validation test for that example.
 \end{adjustwidth}
 
+\bibitem[Lamport 02]{Lamp02} Lamport, Leslie\\
+``Specifying Systems''\\
+\verb|research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf|
+Addison-Wesley ISBN 0-321-14306-X
+
+\bibitem[Newcombe 13]{Newc13} Newcombe, Chris; Rath, Tim; Zhang, Fan;
+Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael\\
+``Use of Formal Methods at Amazon Web Services''\\
+\verb|research.microsoft.com/en-us/um/people/lamport/tla/|
+\verb|formal-methods-amazon.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+In order to find subtle bugs in a system design, it is necessary to
+have a precise description of that design. There are at least two
+major benefits to writing a precise design; the author is forced to
+think more clearly, which helps eliminate ``plausible hand-waving'',
+and tools can be applied to check for errors in the design, even while
+it is being written. In contrast, conventional design documents
+consist of prose, static diagrams, and perhaps pseudo-code in an ad
+hoc untestable language. Such descriptions are far from precise; they
+are often ambiguous, or omit critical aspects such as partial failure
+or the granularity of concurrency (i.e. which constructs are assumed
+to be atomic). At the other end of the spectrum, the final executable
+code is unambiguous, but contains an overwhelming amount of detail. We
+needed to be able to capture the essence of a design in a few hundred
+lines of precise description. As our designs are unavoidably complex,
+we need a highly-expressive language, far above the level of code, but
+with precise semantics. That expressivity must cover real-world
+concurrency and fault-tolerance. And, as we wish to build services
+quickly, we wanted a language that is simple to learn and apply,
+avoiding esoteric concepts. We also very much wanted an existing
+ecosystem of tools.  We found what we were looking for in TLA+, a
+formal specification language.
+\end{adjustwidth}
+
 \bibitem[Poll 99a]{P99a} Poll, Erik\\
 ``The Type System of Axiom''\\
 \verb|www.cs.ru.nl/E.Poll/talks/axiom.pdf|
diff --git a/changelog b/changelog
index b38c4c0..58acd41 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140703 tpd src/axiom-website/patches.html 20140703.04.tpd.patch
+20140703 tpd books/bookvolbib add Lamport book "Specifying Systems"
 20140703 tpd src/axiom-website/patches.html 20140703.03.tpd.patch
 20140703 tpd src/axiom-website/documentation.html add Lamport quote
 20140703 tpd src/axiom-website/patches.html 20140703.02.tpd.patch
diff --git a/patch b/patch
index 3d341cd..906da1e 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,5 @@
-src/axiom-website/documentation.html add Lamport quote
+books/bookvolbib add Lamport book "Specifying Systems"
 
-Mathematics is nature's way of letting you know how sloppy your
-writing is.  Formal mathematics is nature's way of letting you know
-how sloppy your mathematics is.
+Free pdf describing TLA+ model checking software.
+http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
+Part of the effort to begin proving Axiom correct.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index f72b7c0..b954f24 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4524,6 +4524,8 @@ src/axiom-website/documentation.html add W.T. Gowers quote
 books/bookvolbib add Numerical Algorithms section, add Yang14
 <a href="patches/20140703.03.tpd.patch">20140703.03.tpd.patch</a>
 src/axiom-website/documentation.html add Lamport quote
+<a href="patches/20140703.04.tpd.patch">20140703.04.tpd.patch</a>
+books/bookvolbib add Lamport book "Specifying Systems"
  </body>
 </html>