diff --git a/Move.toml b/Move.toml
index 8c0de80..02aa3fe 100644
--- a/Move.toml
+++ b/Move.toml
@@ -10,4 +10,4 @@ PontemFramework = "0x1"
 Root = "0xA550C18"
 
 [dependencies]
-MoveStdlib = { git = "https://github.com/pontem-network/move-stdlib.git", rev = "release-v1.0.0"}
+MoveStdlib = { git = "https://github.com/pontem-network/move-stdlib.git", rev = "new-reflect-module"}
diff --git a/sources/ChainId.move b/sources/ChainId.move
index 7d129e3..2e45d2e 100644
--- a/sources/ChainId.move
+++ b/sources/ChainId.move
@@ -28,8 +28,10 @@ module PontemFramework::ChainId {
         pragma opaque;
         let root_addr = Signer::address_of(root_account);
         modifies global<ChainId>(root_addr);
+
         include PontTimestamp::AbortsIfNotGenesis;
         include CoreAddresses::AbortsIfNotRoot{ account: root_account };
+
         aborts_if exists<ChainId>(root_addr) with Errors::ALREADY_PUBLISHED;
         ensures exists<ChainId>(root_addr);
     }
@@ -48,7 +50,7 @@ module PontemFramework::ChainId {
     /// # Initialization
 
     spec module {
-        /// When Diem is operating, the chain id is always available.
+        /// When Pontem is operating, the chain id is always available.
         invariant [suspendable] PontTimestamp::is_operating() ==> exists<ChainId>(@Root);
 
         // Could also specify that ChainId is not stored on any other address, but it doesn't matter.
diff --git a/sources/PontAccount.move b/sources/PontAccount.move
index 458415c..9e8f005 100644
--- a/sources/PontAccount.move
+++ b/sources/PontAccount.move
@@ -33,7 +33,7 @@ module PontemFramework::PontAccount {
         /// The code symbol for the token that was sent
         symbol: String,
         /// The address that was paid
-        payee: address,
+        to_addr: address,
         /// Metadata associated with the payment
         metadata: vector<u8>,
     }
@@ -45,206 +45,198 @@ module PontemFramework::PontAccount {
         /// The code symbol for the token that was received
         symbol: String,
         /// The address that sent the token
-        payer: address,
+        from_addr: address,
         /// Metadata associated with the payment
         metadata: vector<u8>,
     }
 
-    /// The `PontAccount` resource is not in the required state
-    const ERR_ACCOUNT: u64 = 0;
     /// Tried to deposit a token whose value was zero
-    const ERR_TOKEN_DEPOSIT_IS_ZERO: u64 = 1;
+    const ERR_ZERO_DEPOSIT_AMOUNT: u64 = 1;
     /// The account does not hold a large enough balance in the specified token
     const ERR_INSUFFICIENT_BALANCE: u64 = 2;
     /// Tried to add a balance in a token that this account already has
-    const ERR_ADD_EXISTING_TOKEN: u64 = 3;
+    const ERR_TOKEN_BALANCE_ALREADY_EXISTS: u64 = 3;
     /// Tried to withdraw funds in a token that the account does hold
-    const ERR_PAYER_DOESNT_HOLD_TOKEN: u64 = 4;
+    const ERR_NO_BALANCE_FOR_TOKEN: u64 = 4;
     /// An account cannot be created at the reserved core code address of 0x1
     const ERR_CANNOT_CREATE_AT_CORE_ADDRESS: u64 = 5;
 
-    /// Deposit `Token<TokenType>` to payee account.
-    public fun deposit<TokenType>(payer: &signer, payee: address, token: Token<TokenType>)
+    /// Deposit `Token<TokenType>` to `to_addr` address.
+    public fun deposit_token<TokenType>(to_addr: address, token: Token<TokenType>, from_addr: address)
     acquires PontAccount, Balance {
-        deposit_with_metadata(payer, payee, token, b"")
+        deposit_token_with_metadata(from_addr, to_addr, token, b"")
     }
 
-    public fun deposit_with_metadata<TokenType>(
-        payer_acc: &signer,
-        payee: address,
+    public fun deposit_token_with_metadata<TokenType>(
+        from_addr: address,
+        to_addr: address,
         token: Token<TokenType>,
         metadata: vector<u8>
     ) acquires Balance, PontAccount {
         PontTimestamp::assert_operating();
+        Token::assert_is_token<TokenType>();
 
         // Check that the `token` amount is non-zero
         let token_amount = Token::value(&token);
-        assert!(token_amount > 0, Errors::invalid_argument(ERR_TOKEN_DEPOSIT_IS_ZERO));
+        assert!(token_amount > 0, Errors::invalid_argument(ERR_ZERO_DEPOSIT_AMOUNT));
 
-        // Create signer for payee.
-        let payee_acc = create_signer(payee);
+        // Create signer for `to_addr` to create PontAccount and Balance resources.
+        let to_addr_acc = create_signer(to_addr);
 
-        // Check that an account exists at `payee`
-        if (!exists<PontAccount>(payee)) {
-            add_user_account(&payee_acc);
-        };
+        // Create PontAccount storage for events, if doesn't exist.
+        ensure_pont_account_exists(&to_addr_acc);
 
-        if (!balance_exists<TokenType>(payee)) {
-            add_balance<TokenType>(&payee_acc);
+        if (!has_token_balance<TokenType>(to_addr)) {
+            create_token_balance<TokenType>(&to_addr_acc);
         };
 
         // Deposit the `to_deposit` token
-        Token::deposit(&mut borrow_global_mut<Balance<TokenType>>(payee).token, token);
+        Token::deposit(&mut borrow_global_mut<Balance<TokenType>>(to_addr).token, token);
 
         // Log a received event
         Event::emit_event<ReceivedPaymentEvent>(
-            &mut borrow_global_mut<PontAccount>(payee).received_events,
+            &mut borrow_global_mut<PontAccount>(to_addr).received_events,
             ReceivedPaymentEvent{
                 amount: token_amount,
                 symbol: Token::symbol<TokenType>(),
-                payer: Signer::address_of(payer_acc),
+                from_addr,
                 metadata
             }
         );
     }
-    spec deposit_with_metadata {
-        pragma opaque;
-
-        modifies global<Balance<TokenType>>(payee);
-        include ModifiesPontAccount { account_addr: payee };
-
-        let amount = token.value;
-        let payer = Signer::address_of(payer_acc);
-//        let balance = global<Balance<TokenType>>(payee);
-
-        include DepositAbort<TokenType>{ amount: token.value, payee };
-//        include Token::AbortsIfDepositOverflow<TokenType> { token: global<Balance<TokenType>>(payee).token, check: token };
-
-        include DepositEnsures<TokenType>{ amount };
-//        include DepositEmits<TokenType>{ payer, amount };
-    }
-    spec schema DepositAbort<TokenType> {
-        payee: address;
-        amount: u64;
-
+    spec deposit_token_with_metadata {
         include PontTimestamp::AbortsIfNotOperating;
         include Token::AbortsIfTokenNotRegistered<TokenType>;
+        include AbortsIfCoreAddress { addr: to_addr };
 
-        aborts_if amount == 0 with Errors::INVALID_ARGUMENT;
-        aborts_if !exists<PontAccount>(payee)
-                  && payee == @PontemFramework with Errors::INVALID_ARGUMENT;
-    }
-    spec schema DepositEnsures<TokenType> {
-        payee: address;
-        amount: u64;
+        aborts_if exists<Balance<TokenType>>(to_addr) &&
+                  global<Balance<TokenType>>(to_addr).token.value + token.value > max_u64() with Errors::LIMIT_EXCEEDED;
 
-        ensures exists<PontAccount>(payee);
-        ensures exists<Balance<TokenType>>(payee);
-        ensures old(exists<Balance<TokenType>>(payee)) ==>
-                balance<TokenType>(payee) == old(balance<TokenType>(payee)) + amount;
-    }
-    spec schema DepositEmits<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
-        metadata: vector<u8>;
-        let handle = global<PontAccount>(payee).received_events;
-        let msg = ReceivedPaymentEvent{
-            amount,
-            symbol: Token::spec_symbol<TokenType>(),
-            payer,
-            metadata
-        };
-        emits msg to handle;
+        let deposit_amount = token.value;
+        aborts_if deposit_amount == 0 with Errors::INVALID_ARGUMENT;
+
+        ensures exists<PontAccount>(to_addr);
+        ensures exists<Balance<TokenType>>(to_addr);
+        ensures old(exists<Balance<TokenType>>(to_addr)) ==>
+                balance<TokenType>(to_addr) == old(balance<TokenType>(to_addr)) + deposit_amount;
     }
 
     /// Withdraw `amount` `Token<TokenType>`'s from the account balance and return.
-    public fun withdraw<TokenType>(
-        payer: &signer,
+    public fun withdraw_tokens<TokenType>(
+        from_acc: &signer,
         amount: u64,
     ): Token<TokenType> acquires Balance {
         PontTimestamp::assert_operating();
 
-        let payer_address = Signer::address_of(payer);
-        assert!(exists<Balance<TokenType>>(payer_address), Errors::not_published(ERR_PAYER_DOESNT_HOLD_TOKEN));
+        // Create PontAccount storage for events, if doesn't exist.
+        ensure_pont_account_exists(from_acc);
+
+        let from_acc_addr = Signer::address_of(from_acc);
+        assert!(exists<Balance<TokenType>>(from_acc_addr), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
+
+        let from_acc_balance = borrow_global_mut<Balance<TokenType>>(from_acc_addr);
+
+        let token = &mut from_acc_balance.token;
+        assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
 
-        let account_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
-        withdraw_from_balance<TokenType>(account_balance, amount)
+        Token::withdraw(token, amount)
     }
+    spec withdraw_tokens {
+        include PontTimestamp::AbortsIfNotOperating;
+
+        let from_acc_addr = Signer::address_of(from_acc);
+        include AbortsIfCoreAddress { addr: from_acc_addr };
+        aborts_if !has_token_balance<TokenType>(from_acc_addr) with Errors::NOT_PUBLISHED;
 
-    public fun pay_from<TokenType>(
-        payer: &signer,
-        payee: address,
+        let from_acc_balance = global<Balance<TokenType>>(from_acc_addr);
+        aborts_if Token::value(from_acc_balance.token) < amount with Errors::LIMIT_EXCEEDED;
+
+        ensures exists<PontAccount>(from_acc_addr);
+        ensures exists<Balance<TokenType>>(from_acc_addr);
+        ensures result.value == amount;
+    }
+
+    public fun transfer_tokens<TokenType>(
+        from_acc: &signer,
+        to_addr: address,
         amount: u64,
     ) acquires PontAccount, Balance {
-        pay_from_with_metadata<TokenType>(
-            payer,
-            payee,
+        transfer_tokens_with_metadata<TokenType>(
+            from_acc,
+            to_addr,
             amount,
             b""
         );
     }
+    spec transfer_tokens {
+        include TransferTokenEnsures<TokenType> {
+            from_addr: Signer::address_of(from_acc),
+            to_addr,
+            amount,
+        };
+    }
 
-    /// Withdraw the balance from payer account and deposit to payee.
-    public fun pay_from_with_metadata<TokenType>(
-        payer_acc: &signer,
-        payee: address,
+    /// Withdraw the balance from `from_acc` account and deposit to `to_addr`.
+    public fun transfer_tokens_with_metadata<TokenType>(
+        from_acc: &signer,
+        to_addr: address,
         amount: u64,
         metadata: vector<u8>,
     ) acquires PontAccount, Balance {
-        let withdrawn_tokens = withdraw_from(payer_acc, payee, amount, copy metadata);
-        deposit_with_metadata<TokenType>(
-            payer_acc,
-            payee,
-            withdrawn_tokens,
-            metadata
+        let tokens = withdraw_tokens<TokenType>(from_acc, amount);
+        let from_acc_addr = Signer::address_of(from_acc);
+        deposit_token_with_metadata<TokenType>(
+            from_acc_addr,
+            to_addr,
+            tokens,
+            copy metadata
+        );
+        Event::emit_event<SentPaymentEvent>(
+            &mut borrow_global_mut<PontAccount>(from_acc_addr).sent_events,
+            SentPaymentEvent{
+                amount,
+                symbol: Token::symbol<TokenType>(),
+                to_addr,
+                metadata
+            },
         );
     }
-    spec pay_from_with_metadata {
-        let payer = Signer::address_of(payer_acc);
-        modifies global<PontAccount>(payer);
-        modifies global<PontAccount>(payee);
-        modifies global<Balance<TokenType>>(payer);
-        modifies global<Balance<TokenType>>(payee);
-
-        ensures exists<Balance<TokenType>>(payer);
-        ensures exists<Balance<TokenType>>(payee);
-
-//        include PayFromAbortsIf<TokenType>;
-        include PayFromEnsures<TokenType> { payer, payee };
-//        include PayFromEmits<TokenType>;
+    spec transfer_tokens_with_metadata {
+        include TransferTokenEnsures<TokenType> {
+            from_addr: Signer::address_of(from_acc),
+            to_addr,
+            amount,
+        };
     }
-    spec schema PayFromEnsures<TokenType> {
-        payer: address;
-        payee: address;
+
+    spec schema TransferTokenEnsures<TokenType> {
+        from_addr: address;
+        to_addr: address;
         amount: u64;
-        ensures payer == payee
-                ==> balance<TokenType>(payer) == old(balance<TokenType>(payer));
-        ensures payer != payee
-                ==> balance<TokenType>(payer) == old(balance<TokenType>(payer)) - amount;
-        ensures payer != payee && old(balance_exists<TokenType>(payee))
-                ==> balance<TokenType>(payee) == old(balance<TokenType>(payee)) + amount;
+        ensures exists<PontAccount>(to_addr);
+        ensures from_addr == to_addr
+                ==> balance<TokenType>(from_addr) == old(balance<TokenType>(from_addr));
+        ensures from_addr != to_addr
+                ==> balance<TokenType>(from_addr) == old(balance<TokenType>(from_addr)) - amount;
+        ensures from_addr != to_addr && old(has_token_balance<TokenType>(to_addr))
+                ==> balance<TokenType>(to_addr) == old(balance<TokenType>(to_addr)) + amount;
+        ensures from_addr != to_addr && old(!has_token_balance<TokenType>(to_addr))
+                ==> balance<TokenType>(to_addr) == amount;
     }
-//    spec schema PayFromEmits<TokenType> {
-//        payer: address;
-//        payee: address;
-//        amount: u64;
-//        include DepositEmits<TokenType>{ payer };
-//        include WithdrawFromEmits<TokenType> { payer };
-//    }
 
     /// Return the current balance of the account at `addr`.
     public fun balance<TokenType>(addr: address): u64 acquires Balance {
-        assert!(exists<Balance<TokenType>>(addr), Errors::not_published(ERR_PAYER_DOESNT_HOLD_TOKEN));
-        balance_for(borrow_global<Balance<TokenType>>(addr))
+        assert!(exists<Balance<TokenType>>(addr), Errors::not_published(ERR_NO_BALANCE_FOR_TOKEN));
+        let balance = borrow_global<Balance<TokenType>>(addr);
+        Token::value<TokenType>(&balance.token)
     }
     spec balance {
         aborts_if !exists<Balance<TokenType>>(addr) with Errors::NOT_PUBLISHED;
     }
 
     /// Add a balance of `TokenType` type to the sending account.
-    public fun add_balance<TokenType>(account: &signer) {
-        let addr = Signer::address_of(account);
+    public fun create_token_balance<TokenType>(acc: &signer) {
+        let addr = Signer::address_of(acc);
 
         // aborts if `Token` is not a token type in the system
         Token::assert_is_token<TokenType>();
@@ -252,195 +244,51 @@ module PontemFramework::PontAccount {
         // aborts if this account already has a balance in `Token`
         assert!(
             !exists<Balance<TokenType>>(addr),
-            Errors::already_published(ERR_ADD_EXISTING_TOKEN)
+            Errors::already_published(ERR_TOKEN_BALANCE_ALREADY_EXISTS)
         );
-        move_to(account, Balance<TokenType>{ token: Token::zero<TokenType>() })
+        move_to(acc, Balance<TokenType>{ token: Token::zero<TokenType>() })
     }
-    spec add_balance {
-        /// An account must exist at the address
-        include AddBalanceAborts<TokenType> { account };
+    spec create_token_balance {
+        include Token::AbortsIfTokenNotRegistered<TokenType>;
 
-        let account_addr = Signer::address_of(account);
-        /// `account` cannot have an existing balance in `Token`
-        aborts_if exists<Balance<TokenType>>(account_addr) with Errors::ALREADY_PUBLISHED;
+        let acc_addr = Signer::address_of(acc);
+        aborts_if exists<Balance<TokenType>>(acc_addr) with Errors::ALREADY_PUBLISHED;
 
-        include AddTokenEnsures<TokenType> { account_addr };
-    }
-    spec schema AddBalanceAborts<TokenType> {
-        account: signer;
-        include Token::AbortsIfTokenNotRegistered<TokenType>;
-        /// `account` cannot have an existing balance in `Token`
-        aborts_if exists<Balance<TokenType>>(Signer::address_of(account)) with Errors::ALREADY_PUBLISHED;
-    }
-    spec schema AddTokenEnsures<TokenType> {
-        account_addr: address;
-        modifies global<Balance<TokenType>>(account_addr);
-        // This publishes a `Balance<TokenType>` to the caller's account
-        ensures exists<Balance<TokenType>>(account_addr);
-        ensures global<Balance<TokenType>>(account_addr).token.value == 0;
+        ensures exists<Balance<TokenType>>(acc_addr);
+        ensures balance<TokenType>(acc_addr) == 0;
     }
 
-
     ///////////////////////////////////////////////////////////////////////////
     // General purpose methods
     ///////////////////////////////////////////////////////////////////////////
-    ///
-    /// Helper to return the u64 value of the `balance` for `account`
-    fun balance_for<TokenType>(balance: &Balance<TokenType>): u64 {
-        Token::value<TokenType>(&balance.token)
-    }
-
     /// If `Balance<TokenType>` exists on account.
-    fun balance_exists<TokenType>(account: address): bool {
+    fun has_token_balance<TokenType>(account: address): bool {
         exists<Balance<TokenType>>(account)
     }
 
-    spec schema AbortsIfPontemFrameworkAccount {
-        acc: signer;
-        aborts_if Signer::address_of(acc) == @PontemFramework with Errors::INVALID_ARGUMENT;
-    }
-
-    /// Create a new account.
-    /// Used to automatically create new accounts when needed.
-    fun add_user_account(acc: &signer) {
+    fun ensure_pont_account_exists(acc: &signer) {
+        let addr = Signer::address_of(acc);
         assert!(
-            Signer::address_of(acc) != @PontemFramework,
+            addr != @PontemFramework,
             Errors::invalid_argument(ERR_CANNOT_CREATE_AT_CORE_ADDRESS)
         );
-        move_to(acc, PontAccount{
-            received_events: Event::new_event_handle<ReceivedPaymentEvent>(acc),
-            sent_events: Event::new_event_handle<SentPaymentEvent>(acc),
-        });
-    }
-    spec add_user_account {
-        let account_addr = Signer::address_of(acc);
-        include ModifiesPontAccount { account_addr };
-
-        ensures exists<PontAccount>(account_addr);
-//        include PontemFrameworkAccountAbort { acc };
-    }
-    spec schema ModifiesPontAccount {
-        account_addr: address;
-        modifies global<PontAccount>(account_addr);
-    }
-
-    /// Withdraw `amount` `Token<TokenType>`'s from the account balance.
-    fun withdraw_from<TokenType>(
-        payer_acc: &signer,
-        payee: address,
-        amount: u64,
-        metadata: vector<u8>,
-    ): Token<TokenType> acquires Balance, PontAccount {
-        PontTimestamp::assert_operating();
-
-        let payer_address = Signer::address_of(payer_acc);
-
-        // Check that an account exists at `payee`
-        if (!exists<PontAccount>(payer_address)) {
-            add_user_account(payer_acc);
-        };
-
-        if (!balance_exists<TokenType>(payer_address)) {
-            add_balance<TokenType>(payer_acc);
-        };
-
-        let account_balance = borrow_global_mut<Balance<TokenType>>(payer_address);
-
-        // Load the payer's account and emit an event to record the withdrawal
-        Event::emit_event<SentPaymentEvent>(
-            &mut borrow_global_mut<PontAccount>(payer_address).sent_events,
-            SentPaymentEvent{
-                amount,
-                symbol: Token::symbol<TokenType>(),
-                payee,
-                metadata
-            },
-        );
-        withdraw_from_balance<TokenType>(account_balance, amount)
-    }
-    spec withdraw_from {
-        let payer = Signer::address_of(payer_acc);
-
-        include ModifiesPontAccount { account_addr: payer };
-        modifies global<Balance<TokenType>>(payer);
-
-        include WithdrawFromAborts<TokenType> { payer };
-//        include Token::WithdrawAborts<TokenType> { token: global<Balance<TokenType>>(payer).token, amount };
-
-        ensures exists<PontAccount>(payer);
-        ensures exists<Balance<TokenType>>(payer);
-
-//        ensures TRACE(balance<TokenType>(payer)) == TRACE(old(balance<TokenType>(payer))) - amount;
-//        include WithdrawFromBalanceEnsures<TokenType>{ balance: global<Balance<TokenType>>(payer) };
-//        include WithdrawFromEmits<TokenType> { payer };
-    }
-    spec schema WithdrawFromAborts<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
-
-        include PontTimestamp::AbortsIfNotOperating;
-        include Token::AbortsIfTokenNotRegistered<TokenType>;
-        aborts_if !exists<PontAccount>(payer)
-                  && payer == @PontemFramework with Errors::INVALID_ARGUMENT;
-//        include Token::WithdrawAbortsIf<TokenType> { token: global<Balance<TokenType>>(payer).token, amount };
-    }
-    spec schema WithdrawFromEmits<TokenType> {
-        payer: address;
-        payee: address;
-        amount: u64;
-        metadata: vector<u8>;
-        let handle = global<PontAccount>(payer).sent_events;
-        let msg = SentPaymentEvent{
-            amount,
-            symbol: Token::spec_symbol<TokenType>(),
-            payee,
-            metadata
+        if (!exists<PontAccount>(addr)) {
+            move_to(acc, PontAccount{
+                received_events: Event::new_event_handle<ReceivedPaymentEvent>(acc),
+                sent_events: Event::new_event_handle<SentPaymentEvent>(acc),
+            });
         };
-        emits msg to handle;
     }
-
-    /// Helper to withdraw `amount` from the given account balance and return the withdrawn Diem<Token>
-    fun withdraw_from_balance<TokenType>(
-        balance: &mut Balance<TokenType>,
-        amount: u64
-    ): Token<TokenType> {
-        PontTimestamp::assert_operating();
-
-        let token = &mut balance.token;
-        assert_enough_tokens_available(token, amount);
-
-        Token::withdraw(token, amount)
-    }
-    spec withdraw_from_balance {
-        include PontTimestamp::AbortsIfNotOperating;
-        include Token::WithdrawAborts<TokenType> { token: balance.token, amount };
-
-        include WithdrawFromBalanceEnsures<TokenType>;
-    }
-    spec schema WithdrawFromBalanceEnsures<TokenType> {
-        balance: Balance<TokenType>;
-        amount: u64;
-        result: Token<TokenType>;
-
-        ensures balance.token.value == old(balance.token.value) - amount;
-        ensures result.value == amount;
+    spec ensure_pont_account_exists {
+        let acc_addr = Signer::address_of(acc);
+        include AbortsIfCoreAddress { addr: acc_addr };
+        ensures exists<PontAccount>(acc_addr);
     }
 
-    fun assert_enough_tokens_available<TokenType>(token: &Token<TokenType>, amount: u64) {
-        // Abort if this withdrawal would make the `payer`'s balance go negative
-        assert!(Token::value(token) >= amount, Errors::limit_exceeded(ERR_INSUFFICIENT_BALANCE));
-    }
-    spec assert_enough_tokens_available {
-        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
+    spec schema AbortsIfCoreAddress {
+        addr: address;
+        aborts_if addr == @PontemFramework with Errors::INVALID_ARGUMENT;
     }
 
     native fun create_signer(addr: address): signer;
-    spec create_signer {
-        pragma opaque;
-        aborts_if false;
-        ensures Signer::address_of(result) == addr;
-    }
 }
diff --git a/sources/PontTimestamp.move b/sources/PontTimestamp.move
index 771fcfa..719308b 100644
--- a/sources/PontTimestamp.move
+++ b/sources/PontTimestamp.move
@@ -73,18 +73,6 @@ module PontemFramework::PontTimestamp {
         global<CurrentTimeMicroseconds>(@Root).microseconds / MICRO_CONVERSION_FACTOR
     }
 
-    #[test_only]
-    public fun set_time_microseconds(ms: u64) acquires CurrentTimeMicroseconds {
-        assert!(is_operating(), Errors::invalid_state(ERR_NOT_OPERATING));
-        borrow_global_mut<CurrentTimeMicroseconds>(@Root).microseconds = ms;
-    }
-
-    #[test_only]
-    public fun set_time_seconds(s: u64) acquires CurrentTimeMicroseconds {
-        let microseconds = s * MICRO_CONVERSION_FACTOR;
-        set_time_microseconds(microseconds);
-    }
-
     /// Helper function to determine if Pontem is in genesis state.
     public fun is_genesis(): bool {
         !exists<CurrentTimeMicroseconds>(@Root)
@@ -124,6 +112,18 @@ module PontemFramework::PontTimestamp {
         aborts_if !is_operating() with Errors::INVALID_STATE;
     }
 
+    #[test_only]
+    public fun set_time_microseconds(ms: u64) acquires CurrentTimeMicroseconds {
+        assert!(is_operating(), Errors::invalid_state(ERR_NOT_OPERATING));
+        borrow_global_mut<CurrentTimeMicroseconds>(@Root).microseconds = ms;
+    }
+
+    #[test_only]
+    public fun set_time_seconds(s: u64) acquires CurrentTimeMicroseconds {
+        let microseconds = s * MICRO_CONVERSION_FACTOR;
+        set_time_microseconds(microseconds);
+    }
+
     // ====================
     // Module Specification
     spec module {} // switch documentation context to module level
diff --git a/sources/Token.move b/sources/Token.move
index 8f401c6..da2c9db 100644
--- a/sources/Token.move
+++ b/sources/Token.move
@@ -82,7 +82,7 @@ module PontemFramework::Token {
     /// A property expected of a `TokenInfo` resource didn't hold
     const ERR_TOKEN_INFO: u64 = 1;
     /// A property expected of the token provided didn't hold
-    const ERR_TOKEN: u64 = 2;
+    const ERR_INVALID_TOKEN: u64 = 2;
     /// The destruction of a non-zero token was attempted. Non-zero tokens must be burned.
     const ERR_DESTRUCTION_OF_NONZERO_TOKEN: u64 = 3;
     /// A withdrawal greater than the value of the token was attempted.
@@ -97,8 +97,7 @@ module PontemFramework::Token {
         Token<TokenType> { value: 0 }
     }
     spec zero {
-//        pragma opaque;
-        aborts_if !is_token<TokenType>() with Errors::NOT_PUBLISHED;
+        include AbortsIfTokenNotRegistered<TokenType>;
         ensures result.value == 0;
     }
 
@@ -117,7 +116,7 @@ module PontemFramework::Token {
         (token, other)
     }
     spec split {
-        aborts_if token.value < amount with Errors::LIMIT_EXCEEDED;
+        include AbortsIfTokenValueLessThanAmount<TokenType> { token, amount };
         ensures result_1.value == token.value - amount;
         ensures result_2.value == amount;
     }
@@ -134,15 +133,11 @@ module PontemFramework::Token {
         Token { value: amount }
     }
     spec withdraw {
-        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
-//        include WithdrawAborts<TokenType> { token, amount };
-
+        include AbortsIfTokenValueLessThanAmount<TokenType> { token, amount };
         ensures token.value == old(token.value) - amount;
         ensures result.value == amount;
     }
-    spec schema WithdrawAborts<TokenType> {
+    spec schema AbortsIfTokenValueLessThanAmount<TokenType> {
         token: Token<TokenType>;
         amount: u64;
 
@@ -156,7 +151,6 @@ module PontemFramework::Token {
         withdraw(token, val)
     }
     spec withdraw_all {
-        pragma opaque;
         ensures result.value == old(token.value);
         ensures token.value == 0;
     }
@@ -168,8 +162,7 @@ module PontemFramework::Token {
         token1
     }
     spec join {
-        pragma opaque;
-        aborts_if token1.value + token2.value > max_u64() with Errors::LIMIT_EXCEEDED;
+        include AbortsIfSumMaxU64<TokenType> { token1, token2 };
         ensures result.value == token1.value + token2.value;
     }
 
@@ -178,21 +171,18 @@ module PontemFramework::Token {
     /// The `check` tokens is consumed in the process
     public fun deposit<TokenType>(token: &mut Token<TokenType>, check: Token<TokenType>) {
         let Token { value } = check;
-        assert!(MAX_U64 - token.value >= value, Errors::limit_exceeded(ERR_TOKEN));
+        assert!(MAX_U64 - token.value >= value, Errors::limit_exceeded(ERR_INVALID_TOKEN));
         token.value = token.value + value;
     }
     spec deposit {
-        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
-//        aborts_if false;
-//        include AbortsIfDepositOverflow<TokenType>;
+        include AbortsIfSumMaxU64<TokenType> { token1: token, token2: check };
         ensures token.value == old(token.value) + check.value;
     }
-    spec schema AbortsIfDepositOverflow<TokenType> {
-        token: Token<TokenType>;
-        check: Token<TokenType>;
-        aborts_if token.value + check.value > MAX_U64 with Errors::LIMIT_EXCEEDED;
+    spec schema AbortsIfSumMaxU64<TokenType> {
+        token1: Token<TokenType>;
+        token2: Token<TokenType>;
+
+        aborts_if token1.value + token2.value > max_u64() with Errors::LIMIT_EXCEEDED;
     }
 
     /// Destroy a zero-value token. Calls will fail if the `value` in the passed-in `token` is non-zero
@@ -203,7 +193,6 @@ module PontemFramework::Token {
         assert!(value == 0, Errors::invalid_argument(ERR_DESTRUCTION_OF_NONZERO_TOKEN))
     }
     spec destroy_zero {
-        pragma opaque;
         aborts_if token.value > 0 with Errors::INVALID_ARGUMENT;
     }
 
@@ -236,40 +225,18 @@ module PontemFramework::Token {
         Token<TokenType> { value }
     }
     spec mint {
-        pragma opaque;
         let deployer_addr = get_deployer_addr<TokenType>();
         modifies global<TokenInfo<TokenType>>(deployer_addr);
-        ensures exists<TokenInfo<TokenType>>(deployer_addr);
-        include MintAbortsIf<TokenType> { deployer_addr };
-        include MintEnsures<TokenType>;
-        include MintEmits<TokenType>;
-    }
-    spec schema MintAbortsIf<TokenType> {
-        value: u64;
-        deployer_addr: address;
+
         include AbortsIfTokenNotRegistered<TokenType>;
         let token_info = global<TokenInfo<TokenType>>(deployer_addr);
         aborts_if token_info.total_value + value > max_u128() with Errors::LIMIT_EXCEEDED;
-    }
-    spec schema MintEnsures<TokenType> {
-        value: u64;
-        result: Token<TokenType>;
-        let deployer_addr = get_deployer_addr<TokenType>();
-        let info = global<TokenInfo<TokenType>>(deployer_addr);
-        let post post_info = global<TokenInfo<TokenType>>(deployer_addr);
+
+        let post post_token_info = global<TokenInfo<TokenType>>(deployer_addr);
         ensures exists<TokenInfo<TokenType>>(deployer_addr);
-        ensures post_info == update_field(info, total_value, info.total_value + value);
+        ensures post_token_info == update_field(token_info, total_value, token_info.total_value + value);
         ensures result.value == value;
     }
-    spec schema MintEmits<TokenType> {
-        value: u64;
-        let info = global<TokenInfo<TokenType>>(get_deployer_addr<TokenType>());
-        let msg = MintEvent{
-            amount: value,
-            symbol: info.symbol,
-        };
-        emits msg to info.mint_events;
-    }
 
     /// Burn `to_burn` tokens.
     /// The function requires `BurnCapability`.
@@ -345,12 +312,6 @@ module PontemFramework::Token {
         (MintCapability<TokenType>{}, BurnCapability<TokenType>{})
     }
     spec register_token {
-        include RegisterTokenAbortsIf<TokenType>;
-    }
-    spec schema RegisterTokenAbortsIf<TokenType> {
-        decimals: u8;
-        account: signer;
-
         let acc_addr = Signer::address_of(account);
         aborts_if exists<TokenInfo<TokenType>>(acc_addr) with Errors::ALREADY_PUBLISHED;
         aborts_if acc_addr != get_deployer_addr<TokenType>() with Errors::CUSTOM;
@@ -386,11 +347,6 @@ module PontemFramework::Token {
         let deployer_addr = get_deployer_addr<TokenType>();
         exists<TokenInfo<TokenType>>(deployer_addr)
     }
-    spec is_token {
-//        pragma opaque;
-        pragma verify = false;
-        aborts_if false;
-    }
 
     /// Returns the decimals for the `TokenType` token as defined
     /// in its `TokenInfo`.
@@ -414,7 +370,6 @@ module PontemFramework::Token {
         *&borrow_global<TokenInfo<TokenType>>(get_deployer_addr<TokenType>()).symbol
     }
     spec symbol {
-        pragma opaque;
         include AbortsIfTokenNotRegistered<TokenType>;
         ensures result == spec_symbol<TokenType>();
     }
@@ -431,7 +386,6 @@ module PontemFramework::Token {
         assert!(is_token<TokenType>(), Errors::not_published(ERR_TOKEN_INFO));
     }
     spec assert_is_token {
-        pragma opaque;
         include AbortsIfTokenNotRegistered<TokenType>;
     }
     spec schema AbortsIfTokenNotRegistered<TokenType> {
diff --git a/tests/NativeTokenTests.move b/tests/NativeTokenTests.move
index ea7707d..2cbce2e 100644
--- a/tests/NativeTokenTests.move
+++ b/tests/NativeTokenTests.move
@@ -14,15 +14,16 @@ module PontemFramework::NativeTokenTests {
         let ponts = NOX::mint(&root_acc, 2);
         let ksms = KSM::mint(&root_acc, 3);
 
+        let root_addr = Signer::address_of(&root_acc);
         let user_addr = Signer::address_of(&user_acc);
-        PontAccount::deposit(&root_acc, user_addr, ponts);
-        PontAccount::deposit(&root_acc, user_addr, ksms);
+        PontAccount::deposit_token(user_addr, ponts, root_addr);
+        PontAccount::deposit_token(user_addr, ksms, root_addr);
 
         assert!(PontAccount::balance<NOX>(user_addr) == 2, 1);
         assert!(PontAccount::balance<KSM>(user_addr) == 3, 2);
 
-        let withdrawn_ponts = PontAccount::withdraw<NOX>(&user_acc, 1);
-        let withdrawn_ksms = PontAccount::withdraw<KSM>(&user_acc, 1);
+        let withdrawn_ponts = PontAccount::withdraw_tokens<NOX>(&user_acc, 1);
+        let withdrawn_ksms = PontAccount::withdraw_tokens<KSM>(&user_acc, 1);
 
         assert!(PontAccount::balance<NOX>(user_addr) == 1, 3);
         assert!(PontAccount::balance<KSM>(user_addr) == 2, 4);
diff --git a/tests/PontAccountTests.move b/tests/PontAccountTests.move
index 64b52de..1075591 100644
--- a/tests/PontAccountTests.move
+++ b/tests/PontAccountTests.move
@@ -16,13 +16,13 @@ module PontemFramework::PontAccountTests {
         let ponts = NOX::mint(&root_acc, 10);
         let (ponts_7, ponts_3) = Token::split(ponts, 3);
 
-        PontAccount::deposit(&root_acc, user1_addr, ponts_7);
-        PontAccount::deposit(&root_acc, user2_addr, ponts_3);
+        PontAccount::deposit_token(user1_addr, ponts_7, @Root);
+        PontAccount::deposit_token(user2_addr, ponts_3, @Root);
 
         assert!(PontAccount::balance<NOX>(user1_addr) == 7, 1);
         assert!(PontAccount::balance<NOX>(user2_addr) == 3, 2);
 
-        PontAccount::pay_from<NOX>(&user1_acc, user2_addr, 5);
+        PontAccount::transfer_tokens<NOX>(&user1_acc, user2_addr, 5);
         assert!(PontAccount::balance<NOX>(user1_addr) == 2, 3);
         assert!(PontAccount::balance<NOX>(user2_addr) == 8, 4);
     }
diff --git a/tests/TokenTests.move b/tests/TokenTests.move
index 3ab0e88..bdf95bb 100644
--- a/tests/TokenTests.move
+++ b/tests/TokenTests.move
@@ -43,11 +43,12 @@ module PontemFramework::TokenTests {
         let ucoins = UCOIN::mint(&minter_acc, 10);
         assert!(Token::value(&ucoins) == 10, 1);
 
+        let minter_addr = @0x42;
         let user_addr = Signer::address_of(&user_acc);
-        PontAccount::deposit(&minter_acc, user_addr, ucoins);
+        PontAccount::deposit_token(user_addr, ucoins, minter_addr);
         assert!(PontAccount::balance<UCOIN>(user_addr) == 10, 2);
 
-        let withdrawn_ucoins = PontAccount::withdraw<UCOIN>(&user_acc, 3);
+        let withdrawn_ucoins = PontAccount::withdraw_tokens<UCOIN>(&user_acc, 3);
         assert!(PontAccount::balance<UCOIN>(user_addr) == 7, 2);
 
         UCOIN::burn(&minter_acc, withdrawn_ucoins);