+* <https://symbiyosys.readthedocs.io>
+
+# 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.