Replies - Activity - proxy - Algorand

xGov-18 Coq-avm library for AVM version 8

The coq-avm library, once it is finished will:

• Make it possible to use Coq to prove mathematical properties of Algorand smart contracts
• These proofs can be used in code audits.
• Aid in future TEAL language/op code design.
• Provide formal specifications of the behavior of TEAL scripts.

How to call an app with just a payment?

In theory you could create a smart signature to authorize spending from an account, but it would also need a special transaction, not just a plain send. It is hard to know if it would help you. What do you want to achieve? What are the requirements to fulfill? (missing the big picture)

As far as I understand, app/smart contract code is only “triggered by a specific type of transaction called an Application Call transaction”. (source: Introduction - Algorand Developer Portal)

xGov-24 VoteCoin - GitHub tools

I know this is off-topic here, but this is the first place I see the analogue between encrypted voting and government elections. I’m wondering what problem does encrypted voting solves in reality:

encryption makes it impossible for public to read the votes vs. in elections all the votes can be re…

Coq-avm library

It seems that the initial proposal and document needs some further details to help the community to measure its values. More details are below for those interested:

The aim of the coq-avm library is to provide a toolset that helps developing formal verification proofs for smart contracts.

Differences of K framework and Coq

Here is a more thorough explanation of the differences of K framework and Coq: K vs. Coq as Language Verification Frameworks (Part 1 of 3