FA 1.2 is the fungible token specification for Tezos :
Below is the archetype implementation:
archetype fa12constant totalsupply : nat = 10_000_000asset 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 = caller; 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 (ledger[owner].tokens)}getter getTotalSupply () : nat {return totalsupply}///////////////////////////////////////////////////////////////////////////////// SPECIFICATION///////////////////////////////////////////////////////////////////////////////specification {s1: ledger.sum(tokens) = totalsupply;}specification entry %transfer (%from : address, %to : address, value : nat) {fails {f0 with (msg : string) :let some after_ledger_from = ledger[%from] inmsg = "NotEnoughBalance" andafter_ledger_from.tokens < valueotherwise true;f1 with (msg : string * (nat * nat)) :let some after_allowance_from_caller = allowance[(%from,caller)] inmsg = ("NotEnoughAllowance", ((value, after_allowance_from_caller.amount))) andcaller <> %from andafter_allowance_from_caller.amount < valueotherwise false;}// LEDGER ASSETpostcondition transfer_p1 { // effect on %from nbtokens%from <> %to ->let some before_ledger_from = before.ledger[%from] inlet some after_ledger_from = ledger[%from] inafter_ledger_from = { before_ledger_from withtokens = abs(before_ledger_from.tokens - value)}otherwise false otherwise false}postcondition transfer_p2 { // effect on %to nbtokens%from <> %to ->let some after_ledger_to = ledger[%to] inlet some before_ledger_to = before.ledger[%to] inafter_ledger_to = { before_ledger_to withtokens = before_ledger_to.tokens + value}otherwiseafter_ledger_to = { holder = %to; tokens = value }otherwise false // %to ledger asset exists after transfer}postcondition transfer_p3 {%from = %to -> ledger = before.ledger}postcondition transfer_p4 { // other ledger assets are unchangedforall tokenholder in ledger,tokenholder.holder <> %from ->tokenholder.holder <> %to ->let some before_th = before.ledger[tokenholder.holder] intokenholder = before_thotherwise false // no other ledger is added}postcondition transfer_p5 { // no ledger asset is removedremoved.ledger.isempty()}postcondition transfer_p6 { // number of added asset may be onelet some before_to = before.ledger[%to] inadded.ledger.isempty()otherwiseadded.ledger = [ { holder = %to; tokens = value } ]}// ALLOWANCE ASSETpostcondition transfer_p7 { // effect on allowancecaller <> %from ->let some before_from_caller = before.allowance[(%from,caller)] inlet some after_from_caller = allowance[(%from,caller)] inbefore_from_caller.amount > value ->after_from_caller = { before_from_caller withamount = abs(before_from_caller.amount - value)}otherwise falseotherwise true}postcondition transfer_p8 { // effect on allowancecaller = %from -> allowance = before.allowance}postcondition transfer_p9 { // other allowance assets are unchangedforall a in allowance,a.addr_owner <> %from and a.addr_spender <> caller ->let some before_a = before.allowance[(a.addr_owner, a.addr_spender)] ina = before_aotherwise true}postcondition transfer_p10 { // no allowance is added or removedremoved.allowance.isempty() and added.allowance.isempty()}}specification entry approve(spender : address, value : nat) {fails {f2 with (msg : (string * nat)) :let some allowance_caller_spender = allowance[(caller, spender)] inmsg = ("UnsafeAllowanceChange", allowance_caller_spender.amount) andvalue > 0 andallowance_caller_spender.amount > 0otherwise false;}postcondition approve_p1 { // effect on allowance assetlet some after_allowance_caller_spender = allowance[(caller,spender)] inlet some before_allowance_caller_spender = before.allowance[(caller,spender)] inafter_allowance_caller_spender = { before_allowance_caller_spender withamount = value}otherwiseafter_allowance_caller_spender = { addr_owner = caller; addr_spender = spender; amount = value }otherwise false}postcondition approve_p2 { // other allowance assets are unchangedforall a in allowance,(a.addr_owner, a.addr_spender) <> (caller, spender) ->let some before_a = before.allowance[(a.addr_owner, a.addr_spender)] ina = before_aotherwise false // no other allowance asset is added}postcondition approve_p3 { // added allowancelet some allowance_caller_spender = before.allowance[(caller, spender)] inadded.allowance.isempty()otherwiseadded.allowance = [ { addr_owner = caller; addr_spender = spender; amount = value } ]}postcondition approve_p4 { // no allowance asset is removedremoved.allowance.isempty()}postcondition approve_p5 {ledger = before.ledger}}specification getter getAllowance (owner : address, spender : address) {postcondition getallowance_p1 { // creates one oplength (operations) = 1}postcondition getallowance_p2 { // assets are unchangedledger = before.ledger and allowance = before.allowance}}specification getter getBalance (owner : address) {postcondition getbalance_p1 { // creates one oplength (operations) = 1}postcondition getbalance_p2 { // assets are unchangedledger = before.ledger and allowance = before.allowance}}specification getter getTotalSupply () {postcondition gettotalsupply_p1 { // creates one oplength (operations) = 1}postcondition gettotalsupply_p2 { // assets are unchangedledger = before.ledger and allowance = before.allowance}}