d-asa

beaker

A framework for writing Smart Contracts on Algorand

pyteal-utils

pyteal-utils is a Python library providing reusable utility functions and classes for PyTEAL, the Python language binding for Algorand's Transaction Execution Approval Language (TEAL). It helps developers write more concise and maintainable smart contracts on the Algorand blockchain by abstracting common patterns and operations. ## Key Features - **Inline Assembly** — Inject raw TEAL source code directly into PyTEAL programs for low-level control. - **Math Utilities** — Functions for mathematical operations like factorial, logarithms, exponentiation, min/max, and saturation. - **Storage Helpers** — Classes and methods for working with global and local storage as binary large objects (blobs), with safe getters and defaults. - **String Operations** — Convert between integers and byte strings, extract prefixes/suffixes, and handle uvarint encoding. - **Transaction Checks** — Assertions for common transaction validations like fee minimums, rekeying, and close-to fields. - **Inner Transaction Builders** — Utilities for creating payment and asset transfer inner transactions. ## Philosophy The library aims to reduce boilerplate in Algorand smart contract development by providing tested, reusable components that follow PyTEAL's patterns, allowing developers to focus on contract logic rather than repetitive low-level code.

avm-semantics

KAVM provides a formal, executable specification of the Algorand Virtual Machine (AVM) and its Transaction Execution Approval Language (TEAL) using the K Framework. This enables rigorous property-based testing and formal verification of Algorand smart contracts, helping developers ensure correctness and security. ## Key Features - **Formal Semantics** — Precise, machine-readable specification of AVM and TEAL behavior. - **Property-Based Testing** — Execute concrete simulations to test smart contracts against defined scenarios. - **Formal Verification** — Prove properties of TEAL programs via symbolic execution (planned). - **Python Integration** — `kavm` Python library and CLI for interoperability with Algorand SDK and tooling. - **Rule Coverage Analysis** — Generate metrics to ensure test suites exercise all semantic rules. ## Philosophy KAVM aims to bring the rigor of formal methods to Algorand smart contract development, reducing bugs and vulnerabilities through executable specifications and verification.