Does anyone have examples of what the proof code looks like? When she says it took 400k lines of code to prove 10kLoC (of high complexity) correct, I got really curious what you’re actually writing in that proof code. (Is it as awful and tedious as those numbers make it sound?)
There are some examples in this paper.
There is a version of this talk w/ live video that I saw here: