Coq was around for longer, used in more projects, hence inconsistencies/problems are
much more likely to have been discovered/fixed.
Since it was around longer, it is much more discussed in academia and in engineering
circles, hence it is likely that developers/researchers are more experienced in its
Coq has plenty of useful libraries implemented over the years, more tooling and
also has general purpose mathematics modules.
The coq-avm library targets AVM byte code, not a specific language (TEAL, pyTeal,
etc.), thus language independent (any program that is compiled to AVM byte code
can be used as a source).
Advantages/disadvantages of using K framework:
Specialized framework, potentially more easy to develop executable sematics modules
targetting different languages.
Language specific implementation, it seems to me that KAVM targets the TEAL language
An open source coq-avm library could help in designing new AVM instructions.
Possible to prove compiler consistency (e.g. all programs executed with version 7
provide the same results when they’re executed with version 8).
Utilizing Coq program extraction would make it possible to generate AVM implementations
in the supported languages (e.g. OCaml, Scheme and Haskell). However, since the main
purpose of the library is precision not performance, the extracted programs may not
be the most effective.
Currently coq-avm provides a way to execute and “step through” (debug) 25 of the
AVM version 8 op codes. (Although using this tool might be unintuitive for developers not
familiar with Coq.)
I’ve read up on this as much as I think I’ll be able to understand. I admire wanting to expand the general tool set of Algorand, but I’m not sure about funding this through xGov at this time given the amount requested and that there are currently alternative methods for achieving the same result from what little I understand. That said, I understand very little of this except that it would be a new way to verify AVM development.
I know very little about Coq, since everything I’ve done with regards to formal theorem provers (which mind you, is not a lot) has been on Isabelle…
These type of tools are definitely interesting and needed, but as the application says kAVM was developed as a type of tool to do this (from my high level POV) and afaik it hasn’t become a standard tool used by developers today. So I don’t see how a Coq version would change this. I’m also wondering what the AlgoKit development team inside the foundation is building, and whether or not there might be a duplication of efforts. But I’m by no means qualified enough to make a full evaluation of this application. Also, considering the amount of resources and grants given to RunTime for the the development of kAVM the ask amount (believe it or not) seems to me slightly on the low side.
I am a bit late to comment but I support this proposal. Coq is an excellent tool and language and was actually used for formal verification of algorand consensus GitHub repo and Arxiv paper. I feel that having a coq implementation is more flexible (K limited to TEAL as mentioned in the op) and more community oriented as K is specific to runtime verification (actually I had never heard of it before reading this post) while coq is a well established academically-used language.
Although I think it would be interesting to get in touch with Algorand, Inc directly as they might also work on some coq development for algorand
I’m no specialist in this domain either, but if Coq provides a more widely accepted standard for formal verification that makes it easier, faster, and more cost-efficient to do, I think it’s potentially worthwhile. I’d be interested to hear how much time could be saved by both developers and auditors if this was available.
As others have noted, I do think it would make sense to first check for any existing work in this area by the Inc., Foundation, and/or other known 3rd parties.