(no commit message)

diff --git a/why_a_libresoc.mdwn b/why_a_libresoc.mdwn
index 161040d3d6ac68c20ed5e373d66f97c529f4ec10..8a643f1d0aa23f1b8e76de47762cff8b9c784663 100644 (file)
--- a/why_a_libresoc.mdwn
+++ b/why_a_libresoc.mdwn
@@ -16,7 +16,7 @@ Our LibreSOC will not have backdoors that plague modern [processors](https://www
 
 There is a very real need for reliable safety critical processors (think airplane, smart car, nuclear power plant, pacemaker...).
 LibreSOC posits that it is impossible to trust a processor in a safety critical environment without both access
-to that processor's source and a cycle accurate HDL simulator that guarantees developers their code behaves as they 
-expect. An ISA level simulator is no longer satisfactory.
+to that processor's source, a cycle accurate HDL simulator that guarantees developers their code behaves as they 
+expect, and formal correctness proofs. An ISA level simulator is no longer satisfactory.
 
 Refer to this [IEEE article](https://ieeexplore.ieee.org/document/4519604) by Cyberphysical System expert Ed-Lee for more details.