Harnessing

Occasionally, CVL lacks a feature that is necessary for a complete verification of a contract. We are working to extend the feature set of CVL to cover these cases, but in the mean time we have developed a set of workarounds that we refer to as “harnesses”.

Harnesses involve systematically altering the behavior of the code being verified. They are therefore unsound.

Harnessing by extension

Todo

This technique is currently undocumented. See our OpenZeppelin verification project for an example.

Harnessing by munging

Todo

This technique is currently undocumented. See our OpenZeppelin verification project for an example.