that Amazon paper is talking about design/algorithm verification using formal methods. This does NOT verify that the design or algorithm in question is actually implemented correctly and matches the design perfectly.