Is there any attempt/project to reverse-engineer Bitcoin's reference implementation, not to an informal description (I have found those), rather to a formal specification?
I have tried searching but could not find anything using formal methods, but maybe I am just using the wrong keywords. Thanks for any reference or insight.