Posted by Georgi Guninski on May 14
sorry for OT.
i am trying to convince a client a bit counterintuitive Coq proof about security is valid.
i can make Coq generate .vo certificates that match the source (human forensic would be happy with this part i suppose).
how do i mitigate human forensic analysis of the proof, what the human forensics will look for? any introductory books?
what if the proof is big (about 3GB) and computer generated?
10x.
Source: OT: best practices in formal verification and security
