sync_up: Add meeting notes for tomorrow

[libreriscv.git] / nlnet_2019_formal.mdwn

diff --git a/nlnet_2019_formal.mdwn b/nlnet_2019_formal.mdwn
index 8b4368d142031429f71ecd1725c7ee905c3b8951..1d3cbb4072a86211fb505290e9f3fcf370e5f5dd 100644 (file)
--- a/nlnet_2019_formal.mdwn
+++ b/nlnet_2019_formal.mdwn
@@ -1,5 +1,7 @@
 # NL.net proposal 2019-10-032
 
+* NLNet Project Page <https://nlnet.nl/project/LibreSoC-Proofs/>
+
 ## Project name
 
 The Libre RISC-V SoC, Formal Correctness Proofs
@@ -156,4 +158,17 @@ all picked up the story.  The list is updated and maintained here:
 
 # Management Summary
 
-The Libre RISC-V SoC Project, https://nlnet.nl/project/Libre-RISCV/, is funded by NLNet to reach ASIC-proven status.  As of Dec 2019 It has been in development for a year, and writing comprehensive unit tests has been both a critical part of that process and a major part of the time taken.  Formal Mathematical Proofs turn out to be critical for several reasons: firstly, they are simpler to read and much more comprehensive (100% coverage), saving hugely on development and maintenance; secondly, they're mathematically inviolate.  From a security and trust perspective, both aspects are extremely important.  Firstly: security mistakes are often accidental due to complexity: a reduction in complexity helps avoid mistakes.  Secondly: independent auditing of the processor is a matter of running the formal proofs.  This proposal therefore not only saves on development time, it helps us meet the goal of developing a privacy-respecting processor in a way that is *independently* verifiable.
+The Libre RISC-V SoC Project, https://nlnet.nl/project/Libre-RISCV/, is
+funded by NLNet to reach ASIC-proven status.  As of Dec 2019 It has been
+in development for a year, and writing comprehensive unit tests has been
+both a critical part of that process and a major part of the time taken.
+Formal Mathematical Proofs turn out to be critical for several reasons:
+firstly, they are simpler to read and much more comprehensive (100%
+coverage), saving hugely on development and maintenance; secondly,
+they're mathematically inviolate.  From a security and trust perspective,
+both aspects are extremely important.  Firstly: security mistakes are
+often accidental due to complexity: a reduction in complexity helps
+avoid mistakes.  Secondly: independent auditing of the processor is a
+matter of running the formal proofs.  This proposal therefore not only
+saves on development time, it helps us meet the goal of developing a
+privacy-respecting processor in a way that is *independently* verifiable.