The amount of formally verified code in the moon project now clocks in at 690 LOC, of which ~2/3 is 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

Sign in to participate in the conversation
Scholar Social

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!