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

Scholar Social is a microblogging platform for researchers, grad students, librarians, archivists, undergrads, academically inclined high schoolers, educators of all levels, journal editors, research assistants, professors, administrators—anyone involved in academia who is willing to engage with others respectfully. Read more ...