1. 14
  1.  

  2. 5

    Uses the Lean theorem prover from Microsoft that was designed to work with real-world code with higher automation than what’s typical in proof assistants. They’re aiming at SPARK or Frama-C more than Coq. The embedded subset is actually larger than I saw for some of the automated work in C which basically reduces down to expressions, while loops, and some heap stuff. So, such an approach might already be useful by itself given a fraction of it was useful for C code esp in embedded.

    https://leanprover.github.io/about/

    https://github.com/leanprover/lean

    1. 4

      This could lead to some very solid libraries – HTTP parsers, crypto, JSON parsers, regular expressions – with verified safety and verified runtimes (asymptotic complexity).