And then how do you know the formal definition you give to Cryptol is correct? How do you know that Cryptol correctly transforms the formal definition to a log

And then how do you know the formal definition you give to Cryptol is correct? How do you know that Cryptol correctly transforms the formal definition to a logic circuit? How do you know it correctly transforms your C/Java/Assembly/VHDL to a logic circuit? Its a deep rabbit hole.