One the whole, a fine document. However, please consider the following comment from Hannes Gredler:

i am a bit concerned about the notion of 'destination' throughout the
document.

the document leaves the taste that you can get away by computing
the distance to 'destination' node and compare that with your neighbors
destination nodal distance and thats all you need for determining
loop free paths.

as always the devil is in the details:
the trouble starts with multi-homed prefixes e.g. direct routes
getting advertised into the IGP from different routers.

IMO its not that simple just comparing nodal cost, what you need to
do is to compare the cost of the prefix in order to make sure that a
network path is loop-free.

consider the following example:

-topology

      +---+
      | S |
      +---+
   5 /     \ 4
+---+       +---+
| E |       | N |
+---+       +---+
  |2          |2
+---+       +---+
| B |       | C |
+---+       +---+
   2 \     / 10
      +---+
      | D |
      +---+

-the primary path from (S,D) is via E
-the backup path (via N) fulfills the LFA rule

   dist_opt(N,D) < dist_opt(S,D) + dist_opt(N,S)
         12      <      9        +       4

so far so good - now lets assume that C & D advertise
a 10.0.0.0/30 link address. C does advertise the direct route
with a cost of 100 and D advertises it with a cost of 80.

if the link between (S,E) fails then we have a loop as N
loops back traffic destined to 10.0.0.0/30 to S.

---
i'd like to see a caveat at the very beginning
that the suggested selection procedure (3.6) either does
violate correctness (if implemented with a nodal notion of 'destination'),
or a clarification that LFA has to be implemented with a prefix
notion of 'destination'.

/hannes