# xGov-18 Coq-avm library for AVM version 8 **URL:** \ **Category:** xGov Proposals Pilot\ **Tags:** voting-session-1\ **Created:** [May 23, 2023, 2:58pm UTC](https://forum.algorand.co/t/xgov-18-coq-avm-library-for-avm-version-8/9635 "2023-05-23T14:58:41Z")\ **Posts on this page:** 1\ **Showing post:** 1
**Author:** ![Adri](https://sea2.discourse-cdn.com/flex016/user_avatar/forum.algorand.co/adri/32/2310_2.png) [@Adri](https://forum.algorand.co/u/Adri)\ **Post date:** [May 23, 2023, 2:58pm UTC](https://forum.algorand.co/t/xgov-18-coq-avm-library-for-avm-version-8/9635/1 "2023-05-23T14:58:41Z")
**Author** Mark (@mpetruska) **Category** Tools **Focus Area** Teal **Open-Source** Yes **ALGO Requested** 250000 **Abstract** The aim is to finish the implementation of the coq-avm library for version 8 af the AVM. A summary of the library can be found here: [coq-avm-introduction.pdf][1] **Link for details** > > > \## Clarification > > The aim of the coq-avm library is to provide a toolset that …helps developing > formal verification proofs for smart contracts in Coq. > > A good overview on formal verification can be found here: > https://ethereum.org/en/developers/docs/smart-contracts/formal-verification/ > (although it is Ethereum related, the main concepts still apply). > > \## Dfferences to K framework > > Runtime Verification Inc. created the \[K framework\](https://kframework.org/) also > implemented an > \[AVM semantics module\](https://github.com/runtimeverification/avm-semantics) > that can be used to verify programs that target the AVM. > > How K framework differs from Coq: > \- Coq is a general purpose interactive theorem prover > \- K framework is a specialized semantics framework > \- Coq is developed from the 1980s > \- K framework is fairly new, first publication is around the 2010s > > Advantages/disadvantages of using Coq: > \- Coq is regarded as a highly trusted tool when used with the Coq standard > library (no additional axioms). (See also: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq, https://mathoverflow.net/questions/59520/how-true-are-theorems-proved-by-coq) > \- 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 > use. > \- 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 > only. > > \## Opportunities > > \- 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.) --- _[View the full topic](https://forum.algorand.co/t/xgov-18-coq-avm-library-for-avm-version-8/9635)._