Was there ever a formal verification of the cryptographic implementation contained in the current Ren protocol?
Also, it isn’t clear from the 4 audits published in the Github whether this specific point from the ADBK audit was ever addressed?
Section 4.3, the⇢n,kRNGprotocol is defined very informally in a big contrast with section 2. It is unclear how the shares are created, what kind of ZK proof is involved and so on. No concrete details are provided. The “verify” function is undefined.
The ADBK audit reviews the RZL paper, not the RenVM implementation itself, and that comment is specifically about a part of the paper that the reviewer felt was too undetailed. I don’t think this has any relevance at this time anymore, in 2021, with RenVM being a live system in production, unless Loong and Ross would like to publish the paper in an academic journal.
With regards to formal verification of the RenVM implementation, I’m not sure this has been attempted yet (although I’m not involved in the tech development so can’t confirm).
The last bits of RenVM that aren’t open-sourced yet will over the year also come out so anyone can review it!
