All - 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.
• Potentially pro…

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 solve in reality:

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

Coq-avm library

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). There are some things that are not entirely correct in the summary (part 3). The main problem is that they provide a method of developing operational semantics for …

The key differences between KAVM and coq-avm are the underlying technologies:

• The K framework is “a rewrite-based executable semantic framework”, it specializes in semantics and program execution.
• Coq is a more “general” interactive theorem prover with very good modelling capabilities.