Will the IELE virtual machine make formal verification platforms like CertiK obsolete, or will they be complementary?

While studying Cardano for my recent article, I became highly impressed with what I read about what the implications of the IELE virtual machine will be. I am not an engineer and the information on IELE is quite technical, but from what I understand, IELE will be built in such a way that it uses semantics based compilation to allow developers to write smart contracts in just about any programming language and, more important, do so in a way that they are correct by construction, as formal verification is actually done beforehand.

When this is fully implemented and functional and indeed lives up to its promise, it will be a really unique feature that sets Cardano apart from every other smart contract platform.

Recently, the Formal Verification platform called CertiK is partnering with just about any other large blockchain (e.g. NEO, Ontology, VeChain and ICON). I’m not sure I fully comprehend how CertiK technically works, but from what I understand it basically uses techniques like machine learning to trace existing errors retrospectively.

I can see why it can be useful in the current blockchain field. Iff I understand correctly, IELE will be built in such a way that it prevents programming errors from happening, while CertiK fixes existing errors. This makes me wonder if the IELE virtual machine is indeed successful, does that make services like CertiK obsolete? Or is there a technical reason CertiK may resolve things IELE can’t making them complementary?

Would love to learn more about this, thanks in advance for any answer/discussion!

2 Likes

Great question…this is over my head, but I would love to know the answer!

1 Like