The amount of formally verified code in the moon project now clocks in at 690 LOC, of which ~2/3 is #ACSL annotations.
707 goals are currently proved by qed, alt-ergo, cvc4 and z3, in around four minutes on a laptop..!
Beyond knowing that all loops terminate and all memory accesses are within bounds, I also have numerical bounds on many variables. This helps verify that accumulators are using appropriate integer types and therefore can't overflow
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!