are there any particular properties that we should attempt to verify?
Some initial comments:
high-level plan for now:
do something similar to what we did for Dexter
but... attempt to automate more of the high-level proofs
Some initial thoughts from the meeting:
we should make our report a bit more technical because our target audience is experts
in particular, let's describe the K Framework verification approach in more detail and its limitations --- what can be verified and what cannot be verified
we can use a similar approach to Dexter to the liquidity-baking
they would also like us to validate the lqt_fa12.ligo contract since that will be their liquidity token contract
the client would like this review to be complete before the Grenada protocol goes live which could happen around Aug. 4th --- thus, according to that timeline, we have roughly 7 weeks
Some initial questions:
Some initial comments:
Some initial thoughts from the meeting: