> an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls.
System calls? How do they come into the picture? And wouldn't reasoning about system calls require proofs about the kernel itself?
Of course, in theory there might be some kernel bug such that e.g. a read() sometimes changes files on disk, but I guess this is outside the scope of that proof system. Only the blog program itself was proven, assuming that the remaining system software as well as hardware are working in a sane way.
If you want your proofs to include the whole operating system, you'd first have to reduce the kernel to a minimal operating system (e.g. MirageOS). If have lots of time, money and motivation, you could continue to include the possibly used virtualization layer (XEN, QEMU/KVM, whatever) and finally the hardware design.
More exactly, we check that the only calls when the user is not logged in are: ReadFile, ListPosts or Log: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...