Have any non-Carnegie Mellon professors or academics verified hashgraph as asynchronous Byzantine fault tolerant (ABFT)?

The hashgraph consensus algorithm has been validated as asynchronous Byzantine fault tolerant by a math proof checked by computer using Coq, a formal proof verification system. Coq provides a formal language to write mathematical definitions and executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. It is often used for certifying the properties of programs, programming languages, and mathematics. The Coq proof of hashgraph was completed by a Carnegie Mellon associate professor of Computer Science. We are not aware of any professors or academics from other institutions who have conducted a Coq analysis of hashgraph, but given the Coq proof is a computer-checked proof (and thus avoids human error) and verified hashgraph as ABFT, we think academics are unlikely to see a reason to verify the proof again. The formalized proof is available at: https://www.hedera.com/hashgraph-coq.zip