# xGov-18 Coq-avm library for AVM version 8

## xGov Proposals Pilot

**Date**: Aug 1, 2023

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](https://github.com/runtimeverification/algorand-verification/tree/release-1.1) and [Arxiv paper](https://arxiv.org/abs/1907.05523). I feel that having a Coq implementation is more flexible (K limited to TEAL as mentioned in the op) and more ...