Verified kernels, written in Dafny and compiled to JavaScript, for correct-by-construction state in interactive web applications