Skip to main content

FA 1.2


A fungible token is basically an association table between the token owner (the account address) and the amount of tokens (a natural integer). It is possible to allow another account to transfer tokens on your behalf.

This contract implements the Financial Asset 1.2 (FA 1.2) TZIP 7 specification for fungible token on Tezos.



totalsupplynatTotal number of tokens.
ledgercollectionAssociation between token holder and number of tokens.
allowancecollectionAssociation between the pair owner and spender and the allowed amount.


transferfrom, to, valueTransfers value tokens from from to to. If the caller is not equal to from, then caller must have been allowed by from to transfer this amount to to.
approvespender, valueApproves spender to transfer value tokens from caller.
getAllowanceowner, spenderGetter for the allowed value for owner and spender.
getBalanceownerGetter for the number of tokens owned by owner.
getTotalSupplyGetter for totalsupply


Originate a FA 1.2 contract with the widget below.

Click "Connect to Wallet" button, fill the fields "Initial Holder" and "Total Supply", and click "Originate".

Token symbol, like 'USD' for United States Dollar.

Token name, like 'Bitcoin' for BTC asset.

A number of decimal places after point.

Image URL for token logo.

Command line

Originate the contract from Archetype code below with the following Completium CLI example command:

completium-cli deploy fa12.arl --init '(@tz1LLJ3nxbpGGMLmjzcp9sTMYui87tycG6nG, 10_000_000)'

The command sets:

  • initialholder constant to tz1LLJ3nxbpGGMLmjzcp9sTMYui87tycG6nG
  • totalsupply variable to 10 millions



The Archetype FA 1.2 code has been verified towards the formal specification presented below.

archetype fa12(initialholder : address, totalsupply : nat)

asset allowance identified by addr_owner addr_spender to big_map {
addr_owner : address;
addr_spender : address;
amount : nat;

asset ledger identified by holder to big_map {
holder : address;
tokens : nat = 0;
} initialized by {
{ holder = initialholder; tokens = totalsupply }

entry %transfer (%from : address, %to : address, value : nat) {
require {
r1 otherwise "NotEnoughBalance" : ledger[%from].tokens >= value;
effect {
if caller <> %from then (
var current = allowance[(%from, caller)].amount;
dofailif(current < value, ("NotEnoughAllowance", ((value, current))));
allowance.update((%from, caller), { amount -= value });
ledger.update(%from, { tokens -= value });
ledger.addupdate(%to, { tokens += value });

entry approve(spender : address, value : nat) {
var k = (caller, spender);
if allowance.contains(k) then (
var previous = allowance[k].amount;
dofailif(previous > 0 and value > 0, (("UnsafeAllowanceChange", previous)));
allowance.addupdate( k, { amount = value });

getter getAllowance (owner : address, spender : address) : nat {
return (allowance[(owner, spender)].amount)

getter getBalance (owner : address) : nat {
return (if (ledger.contains(owner)) then ledger[owner].tokens else 0)

getter getTotalSupply () : nat {
return totalsupply