OT: best practices in formal verification and security

[Georgi Guninski <guninski () guninski com>]

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.

_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/