<story><title>How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors</title><url>https://consensys.net/blog/ethereum-2-0/20039/</url></story><parent_chain><item><author>Taikonerd</author><text>You know, I&amp;#x27;m not really into cryptocurrency, but it does seem like it&amp;#x27;s contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!</text></item></parent_chain><comment><author>tombert</author><text>I agree; I&amp;#x27;ve been trying to get employers&amp;#x2F;coworkers to look into TLA+ or Isabelle (for different things) for years now, and it feels like only after every cryptocurrency started blogging did they start to listen.&lt;p&gt;I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual &lt;i&gt;banks&lt;/i&gt; don&amp;#x27;t seem to have these same requirements.&lt;p&gt;NOTE: Could be wrong on that last point, getting my information about banks third-hand, it&amp;#x27;s possible that banks are using formal verification.  Can someone who works at a bank confirm?</text></comment>
<story><title>How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors</title><url>https://consensys.net/blog/ethereum-2-0/20039/</url></story><parent_chain><item><author>Taikonerd</author><text>You know, I&amp;#x27;m not really into cryptocurrency, but it does seem like it&amp;#x27;s contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!</text></item></parent_chain><comment><author>galangalalgol</author><text>I&amp;#x27;ve worked on safety critical software, but we did not use formal methods. Lots of test and checking for coverage (at asm level). Oodles of static analysis and wading through false positives. Do formal methods usually supplement those or replace some of it?  Can provers or formal methodologies scale to safety critical codebases of 100s of ksloc? Whether such codebases should exist, or be better partitioned is a separate issue.</text></comment>