correct by construction engineering approach: footnote?

[dckc]

I wonder if some sort of footnote is appropriate for the Mercury time-frame:

Since the contract language and its VM are build [sic] from the formal specifications of provable mathematics, and since the compiler pipeline and engineering approach is correct by construction, we expect the platform will be regarded as trustworthy.

I see some K framework stuff for Rholang has been started, but for the VM, we have thousands of lines of code before anyone even attempted to state the correctness theorem, yes?