Lean proved this program was correct; then I found a bug (by kirancodes) — discussion
#formalmethods #plt #security
