Formal Verification

[aleeusgr]

• format

CoQ, yices, Z3 and the whole world of tools and methods.
I think I have a good book in my old laptop, any heads up on tooling to look into?

Or contract model is all you need?

Thank you, 🙏

CoQ is far from being automated 😅 yices and z3 would need to do some development to translate from Plutus (or another programming language) to SMT lib and embedding the behavior of the ledger as well

https://discord.com/channels/1029837832350605343/1030116075532206101/1097197231909646447

[aleeusgr]

DJED used Isabelle

<@454007399469285396> why do you expect the proofs to be automatic? Usually, one wants to prove complex statements about smart contracts.
Also, in the case of Djed they used Isabelle. Would you expect to do these proofs with something like why3 or dafny?

Yes, I know this should be level 3, but have the details been worked out for how the certificates would be stored? E.g. Isabelle proofs in ipfs?

Our concert framework (in Coq) works well for functional contracts in the account model. It should be possible to adapt it to the eutxo model (in fact someone started doing that). It should also be possible to get a (more) verified compiler for plutus out of this.
https://github.com/AU-COBRA/ConCert

[aleeusgr]

I was a bit too quick in my answer. I think there should be space for all kinds of formal verification. I know that a lot of people are working with theorem provers and I really like this area of work. I think this often brings the possibility to prove complex security properties.

That being said, I worked previously on moving away from Coq-based verification to code-level deductive verification for a new release of a product and a high level security certification so I believe it’s possible to do very strong verification without Coq, Isabelle or the likes. And indeed we used something that relied on Why3.

It’s just that I think we are currently missing by not having model checking or indeed bridges to Dafny or Why3 in our ecosystem. Formal verification that would also work at code level and provide automated formal verification with simple assertions. Djed did some work on formalizing to Lustre and use Kind2 to model check their contract. From my previous experience this is often a good way to bring FM to many developers even if you might not be able to prove everything you want.

We’re working on having a mechanism to store the certificate on-chain and we’ll have to refine what we require for L3.

I really like what you’re doing with ConCert and I would really like to take some time in the future to experiment with it 🙂

Do you imagine proving functional properties with why3/dafny, or properties about utxos? I'm not sure I've seen those automatic provers applied a lot to functional languages, but that may just be because I haven't looked for them.

Yes, I agree we should combine a collection of FM tools to work on the same program.
This is what we are doing with high assurance cryptography
https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf
we're extending this work to rust smart contracts.
BTW I thought midnight would also be using rust. Is any more information available?

I'd really like to prove functional properties and even things about execution traces!
This is true that they haven't been used on a lot of functional languages. I'm aware of Cameleer for OCaml https://arxiv.org/abs/2104.11050 I've discussed with people involved in Why3 and they think something should be doable.

I'll check about rust and its use in Midnight

I'd really like to prove functional properties and even things about execution traces!
This is true that they haven't been used on a lot of functional languages. I'm aware of Cameleer for OCaml https://arxiv.org/abs/2104.11050 I've discussed with people involved in Why3 and they think something should be doable.

I'll check about rust and its use in Midnight