# Towards Proxy Staking Accounts Based on NFTs in Ethereum

Viktor Valaštín, Roman Bitarovský, Kristián Košťál and Ivan Kotuliak  Faculty
of Informatics and Information Technologies
Slovak University of Technology in Bratislava
Bratislava, Slovakia
{viktor.valastin, xbitarovsky, kristian.kostal<EMAIL_ADDRESS>
###### Abstract

Blockchain is a technology that is often used to share data and assets.
However, in the decentralized ecosystem, blockchain-based systems can be
utilized to share information and assets without the traditional barriers
associated with solo responsibility, e.g., multi-sig wallets. This paper
describes an innovative approach to blockchain networks based on a non-
fungible token that behaves as an account (NFTAA). The key novelty of this
article is using NFTAA to leverage the unique properties of NFTs to manage
your ownership better and effectively isolate them to improve the security,
transparency, and even interoperability possibilities. Additionally, the
account-based solution gives us the ability and flexibility to cover regular
use cases such as staking and liquid equities, but also practical
composability. This article offers a simple implementation, which allows
developers and researchers to choose the best solution for their needs in
demand of abstract representation in any use case.

###### Index Terms:

proxy accounts, non-fungible tokens, NFTAA, solidity, liquidity

##  I Introduction

When Ethereum transitioned to the Proof-of-Stake consensus, it was a huge
signal for the ecosystem [1]. This switch from the Proof-of-Work (PoW)
consensus mechanism is being done for several reasons. Firstly, PoS is more
energy efficient and environmentally friendly than PoW [2]. It also allows for
faster transaction processing and improved scalability. PoS allows for more
decentralized decision-making, as the power to validate transactions is
distributed among multiple ”mining” nodes rather than concentrated in a few
large mining pools [3].

To ensure correct protocol mechanisms, asset staking was invented. Staking
refers to holding and committing assets as collateral to participate in the
validation of transactions and the production of new blocks. Stakers, also
known as validators, are producing new blocks for blockchain. If a validator
produces a valid block, they are rewarded with a portion of the transaction
fees and a block reward. However, if they produce an invalid block, they may
be penalized, and their staked assets may be slashed.

Yet, staking has a few problems, and in addition to discussing and speculating
about its decentralization or securing, one of them is the illiquidity of
staked assets and the impossibility of changing their owner. The inability to
change the owner of staked assets can be very inconvenient, for example, if we
urgently need to exchange our current staked collateral for other assets. This
paper closely looks at this problem, analyzes the existing solutions, and
describes a new concept that introduces the staking assets through an NFT
account (NFTAA), i.e., transferring the ownership of the stake to the NFT
account, which allows changing the owner of the stake (through a change of
ownership of the NFTAA) in case that we need.

The rest of the paper is organized as follows: In Section II, a closer look at
the example of Ethereum and its technical specifications is provided. Existing
related works are analyzed in Section III. Next, the solution is presented in
the form of NFT proxy accounts described in Section IV, and our evaluation is
described in Section V. We summarize the paper, the discussion, and future
work in Section VI.

##  II Ethereum introduction

Ethereum stands tall as the unrivaled titan in the realm of smart contract
platforms, commanding its position as the foremost and most sophisticated hub
for decentralized financial ecosystems across the globe.

This pioneering blockchain network is purpose-built to facilitate the seamless
operation of decentralized applications (dApps) while steadfastly pursuing
continuous enhancements in scalability, an ongoing mission undertaken by its
vibrant community of developers and stakeholders. Ethereum’s commitment to
scalability underscores its unwavering dedication to delivering a future-proof
infrastructure that can efficiently accommodate the ever-expanding demands of
the decentralized world. Through its tireless innovation, Ethereum endeavors
to remain the largest, most adaptable, and responsive smart contract platform,
serving as the bedrock of the decentralized digital economy.

###  II-A Proof of stake

In proof of stake (PoS), compared to proof of work (PoW) used in Bitcoin, we
do not have miners but rather validators. Validators are nodes that validate
blocks and their data, such as transactions. Validators are not competing to
find the correct hash for a block and do not receive a reward in the form of a
coinbase transaction as miners in Bitcoin. Instead, validators receive a
reward through transaction fees from the transactions included in the block
they validate. Having a lot of computing power to be a validator is
unnecessary, and the process is less energy-intensive [4].

Validators are motivated to refrain from cheating because they must stake a
certain amount of coins to become validators. These staked coins are used to
secure the network and safeguard against cheating. If a validator is caught
cheating, they lose their staked coins and can no longer serve as a validator.
Since the reward for validating a block is typically less than the amount of
staked coins, it is not financially worthwhile for a validator to cheat. In
Ethereum, the amount of staked coins required to become a validator is set at
32 ETH [5]. Staking this amount is quick; however, unstaking is slightly
different and can take days; recently, it was more than five days [6].
Therefore, selling the account with staked 32 ETH is quicker and gives users
easy and fast access to money. However, you do not want to sell your original
account because you could have history and other liquidity associated with it.
Thus, we are introducing staking through an NFT which works as a proxy and
isolates your stake, so you can easily sell it to anyone without risk of
selling more than your stake.

##  III Related work and Background

As mentioned, proof-of-stake can provide security for the network by other
participants. As a bonus, there is also gaining of some profit from the
staking. However, PoS has some drawbacks. First, to unstake the tokens, there
is a need to wait for the withdrawal period.

The current withdrawal mechanism for validators has shown significant
scalability concerns as the network grows. At present, the system only
accommodates 16 withdrawals within a single block. This translates to a
maximum processing capability of 115,200 validator withdrawals daily under the
ideal scenario of no missed slots. This limitation becomes particularly
pronounced in light of rising validator numbers: 800,000 withdrawals take an
entire week to process. This rigid structure poses a severe challenge as it
correlates the number of validators with the withdrawal processing time.

Moreover, the inherent risk of missed slots further complicates the landscape.
While the system is designed to bypass validators without eligible
withdrawals, thereby potentially saving some time, the downside of missed
slots has a pronounced effect. Each missed slot can lead to a proportional
delay in processing, pushing the timeline even further. Such inefficiencies
can negatively impact user experience, potentially dissuading prospective
validators from participating and undermining the very foundation of the
network’s decentralization principle. This bottleneck, if not addressed,
threatens both the operational efficacy and the perceived reliability of the
platform.

Fortunately, already existing solutions can help solve these problems.
Generally speaking, there is a familiar concept: Lock ETHs and get a token
representing the staked amount (derivate). Getting derivate from the staked
asset is also called liquid staking. It represents the idea of making locked
assets liquid. A liquid asset represents an asset that can be converted to
cash. In DeFi terms, liquid assets can be swapped for other assets, such as
stablecoins, or provide additional liquidity on the various decentralized
exchanges.

###  III-A Liquid Staking Protocols

Liquid staking providers empower you to tap into the liquidity of your staked
assets. In return, these providers typically claim a share of the staking
rewards ranging from 5% to 10% as compensation for rendering this valuable
service. With the Shanghai upgrade, the appeal of Ethereum Liquid Staking
Derivatives (LSDs) is set to soar, as it alleviates the inherent risks and
inconveniences associated with conventional ETH staking. This surge in LSD
adoption translates into amplified revenue streams for liquid staking
platforms, instilling a bullish sentiment across the liquid staking sector.
Anticipating this upward trajectory, MetaMask has thoughtfully integrated
staking directly into its wallet interface, streamlining the process for users
to stake their ETH. Users can look forward to earning approximately 5% annual
rewards in ETH by leveraging this feature, with support currently extended to
Lido and Rocket Pool and the possibility of more integrations in the pipeline
[7].

###  III-B Lido

Lido made its mark as a trailblazer in the field of liquid staking. In 2020,
with the launch of Ethereum’s Beacon chain, Lido became the first provider to
offer liquid staking services, pioneering and popularizing this innovative
approach. Since its inception, Lido has consistently maintained its position
as a market leader.

Lido’s liquid staking solution revolves around its token known as stETH, which
represents users’ staked Ethereum (ETH). The process is simple: users deposit
their ETH on Lido’s staking platform and receive stETH in return. This
transformative token empowers users by preserving the liquidity of their
staked assets. With stETH in hand, users can explore a myriad of DeFi
opportunities. Holders of stETH can choose to engage in various DeFi
activities, including trading, lending, providing liquidity, and using it as
collateral. Additionally, stETH holders earn ETH staking rewards in the form
of more stETH tokens, further enhancing their potential yield.

Lido operates on a sustainable revenue model. The platform collects a 10% fee
from the ETH staking rewards generated. This fee is divided between Lido’s
node operators, who ensure the network’s security, and the DAO (Decentralized
Autonomous Organization) treasury.

Despite its outstanding achievements, Lido’s dominant position has raised
concerns within the Ethereum community. Concentrating a substantial amount of
Ether within a single organization poses potential risks to the network. A
centralized attack on the Ethereum network could become feasible if Lido’s
control surpasses 33%. This scenario, known as a 1/3 centralization attack, is
a recognized challenge in Proof-of-Stake ecosystems. In response, Lido and the
Ethereum community are actively exploring avenues to enhance the
decentralization of the protocol, mitigating these potential risks [7, 8].

###  III-C Rocket Pool

Rocket Pool is a groundbreaking Ethereum PoS protocol designed to be
community-owned, decentralized, trustless, and compatible with Ethereum’s
staking system. The project was conceived in late 2016 and has been live since
October 2021. Rocket Pool caters to two primary user groups:

  * •

Tokenized Stakers: Individuals who want to participate in Ethereum staking
using rETH with deposits as low as 0.01 ETH.

  * •

Node Operators: Users who stake ETH and run a node in the Rocket Pool network
to earn higher returns compared to staking independently outside the protocol.
This includes experienced users and those who may not have 32 ETH for solo
staking.

The core premise of Rocket Pool is to ensure the network remains
decentralized, aligning with Ethereum’s ethos and promoting self-sovereignty.
Rocket Pool comprises several key components that create a decentralized
Ethereum staking ecosystem. Smart contracts facilitate ETH deposits, allocate
them to node operators based on demand, and manage various tokens and rewards.
Rocket Pool’s decentralized network of specialized Ethereum nodes runs the
Smart Node software. These nodes communicate with the protocol’s smart
contracts and provide the network consensus required by the Ethereum Beacon
Chain. Minipool validators are smart contracts created by node operators who
deposit 8 or 16 ETH on their node. When the total ETH in a Minipool validator
reaches 32 ETH, a new validator is created to perform consensus duties.

Rocket Pool’s commitment to decentralization, security, and inclusivity makes
it an attractive solution for those looking to participate in Ethereum staking
without the traditional barriers associated with solo staking. The
decentralized protocol ensures resilience, scalability, and more equitable
distribution of rewards within the network [7, 9].

###  III-D EIP-6551

The world of non-fungible tokens (NFTs) is on the brink of a significant
transformation with the introduction of the ERC-6551 token standard. This new
standard seeks to enhance the functionality of NFTs by equipping them with
smart contract capabilities, allowing them to represent unique digital assets
and act as smart contract wallets. The ERC-721 standard, the foundation for
creating unique digital assets on the Ethereum blockchain, has its
limitations. While it paved the way for myriad applications, from art to
virtual real estate, its scope is restricted. NFTs based on ERC-721 can only
be owned and transferred; they cannot own other assets or interact dynamically
with other smart contracts. Proposed as an Ethereum Improvement Proposal (EIP)
in February 2023, ERC-6551 aims to address these limitations. It introduces a
system where every NFT can be assigned an Ethereum account, termed a token-
bound account (TBA). This account enables the NFT to own assets, interact with
applications, and execute arbitrary operations, all without necessitating
changes to existing smart contracts or infrastructure. Key features:

  * •

Smart Contract Capabilities: Beyond representing unique assets, ERC-6551
tokens can function as smart contract wallets, holding other tokens and NFTs.

  * •

Interactivity: TBAs can seamlessly interact with various entities on the
Ethereum network, from decentralized exchanges to gaming platforms.

  * •

Composability: This feature allows NFTs to bundle with related assets,
enhancing user experiences, especially in Web3 gaming environments.

  * •

Identity & Provenance: Each NFT, with its distinct identity, can interact
independently with decentralized applications (dApps). Additionally, users can
trace the complete transaction history of an asset, offering a clearer picture
of its past interactions and uses.

The ERC-6551 standard represents a pivotal moment in the evolution of NFTs.
Bridging the gap between unique digital assets and smart contract
functionality opens up a realm of possibilities in the Web3 space, from gaming
to art and beyond. As the crypto community navigates its challenges, the
potential of ERC-6551 to redefine digital ownership remains immense [10, 11,
12].

But this solution also has some gaps. Firstly, the existence of TBA is not
documented in the NFT, meaning we could possess an NFT without any knowledge
of an associated account until we check the TBA register. We can also sell an
NFT with possession of different assets by mistake and thus lose our precious
liquidity. The second major gap is the lack of atomicity in the creation
process. Of course, this is because TBA applies to all existing NFTs. Still,
we think that creating an NFT and wallet in one atomic transaction, ensuring
that the NFT is fully bound to the wallet proxy contract from its inception
and that the NFT has information about its connection to the wallet contract,
is more transparent.

##  IV Solution design

In the case of the existing solutions (except ERC-6551), the ETH collateral is
often protected via a DAO / multi-signature account. However, this means that
the security of the assets is not directly in the hands of the user because,
in case of a problem or a third-party devaluation, our liquid assets
representing our stake are depreciated. This section delves into the cutting-
edge notion of staking via NFTs, which serve as distinct accounts within the
system. Although this method is not yet common, we bring a few insights into
why it is a good idea. As we see it as a non-standard idea, the novelty of our
work lies in exploring its potential, while considering this rarity not as a
weakness, but as an opportunity to innovate in the field of blockchain
applications.

The term ”non-fungible token” refers to a unique and distinct asset that can
represent various physical items with varying values. On the other hand, NFTs
primarily operate on the asset side of the owner-asset relationship and lack
the potential to own other assets. On the other hand, accounts are used to
represent ownership of assets. In an owner-asset relationship, the account can
be on the first or second side. After composing these two relations, it
follows that it is possible for an account and an NFT to be represented by a
single object that will be uniquely identifiable and will have the nature of
an asset that can be owned - change its owner and at the same time can own
other assets. We represent a non-fungible token as an account, NFTAA in short.
Most Ethereum is based on a single account architecture consistent with the
NFTAA philosophy and facilitates connection with existing infrastructure. We
may easily exploit existing infrastructure for smooth communication if NFTAAs
are handled as conventional accounts. Furthermore, if needed, NFTAAs can
function as asset owners or in a multi-sig scheme.

Another key characteristic of NFTAA is the ownership possibilities and the
transferability of this ownership to any other account, potentially other
NFTAAs. This means that the private keys used to alter a certain NFTAA will
change. This is feasible thanks to the well-known proxy smart contracts [13,
14]. Figure 1 shows the relationships between NFTAA and other logical
entities.

Figure 1: NFT as an account interaction

We can create a proxy account (smart contract) to perform specific tasks on
behalf of another account. For example, Bob’s account can have a proxy account
named Alice. Alice can send transactions on Bob’s behalf, but only for the
calls Bob has approved, as Bob is the only person currently authorized to
access the proxy. This means that if Alice sends a transaction, it is
initiated by Bob, so Bob appears to be signed by Bob, even though Alice is
technically sending it.

Figure 2: NFTAA Solidity sequence diagram

###  IV-A DeFi and DAO use cases

When we discuss accounts, NFTs, assets, staking, ownership, and owners - DeFi
comes into play, and because of the nature of NFTAA, we will also discuss DAO.
As stated before, if we own ETH and decide on liquidity staking, we have
staked the ETH in exchange for other assets we can continue utilizing.
Compared to futures or tokens as a reward for staking, NFT may appear to be
one large illiquid piece of value. This is not the case because
fractionalizing NFT is not novel in the DeFi world [15]. The ideal number of
fractions equals the number of ETH tokens staked on behalf of the NFTAA
account. However, for whatever reason, we may be unable to fold NFTs
distributed in this manner back to their original condition. We could remedy
this by holding a buyout auction or depositing a sum greater than the reported
staking value. We can still perform an unstake if our NFTAA becomes fully
illiquid for any reason and cannot be sold on the secondary market or used as
collateral for a loan, and after this, the NFTAA may (or may not) be burnt.

Another intriguing application of NFTAA is the ability to manage an account
using numerous proxy accounts, each with the capacity to make certain calls.
This offers numerous benefits as we see it as a new paradigm for asset
management and ownership in the ecosystem of decentralized finances. We can
think of NFTAA as a company with employees who have specific roles. Specific
subaccounts represent particular roles, but the company signs all
transactions. From another point of view, NFTAA represents a company that can
hold shares in the form of investments and other liquid or unique assets.
NFTAA, like any other corporation, can be acquired. The NFTAA also functions
as the company’s ledger.

Last but not least, the big trend in the Ethereum ecosystem is re-staking
liquid staking tokens (LRST), such as Lido and Rocket Pool mentioned in
Section III as re-staked tokens serve as a security for data availability
layers - mainly dominated by EigenLayer [16]. We open new possibilities and
scientific contributions of LRSTs because the NFTs can give better portfolio
control without emitting new tokens for re-staking.

###  IV-B Architecture

Figure 2 shows the key elements of the architecture. The foundation of the
entire implementation is the NFTAA smart contract, which has ERC-721 as the
underlying implementation. Subsequently, the NFT mining functionality is
enriched by the creation of the NFTAA smart contract, which is interleaved
from the NFT that has been mined. The NFTAA contract contains a proxy function
that allows the owner of the pinned NFT to perform transactions through the
NFTAA account.

Listing 1 shows how we can modify a function to be successfully called only if
the caller owns a bound NFT.

⬇

1modifier onlyNFTOwner() {

2 require(

3 msg.sender == ERC721(_binded_nft_addr).ownerOf(_binded_nft_id),

4 "Caller is not the owner of the NFT"

5 );

6 _;

7}

Listing 1: NFT owner only modifier

We created a web application that allows users to engage with the NFTAA
manufacturing contract. The application is built on a template for developing
web apps that interface with web3 applications [17]. This template is useful,
but it only works with the Talisman wallet. Unfortunately, the Talisman
documentation does not state if it allows signing EVM transactions [18, 19].
To alleviate this constraint, we have added Metamask wallet support. Finally,
for ease of use, as we can see in Figure 3, we created a dApp using the NFTAA
concept for staking. Via this decentralized application, we can: Stake, Add
other funds to the stake, Unstake, Get a balance of the stake, Get the staker
address, Mint new NFTAA, Transfer ownership of NFTAA.

Figure 3: NFTAA dApp

NFTAA introduces a novel approach to account management. Each user is issued a
unique NFT that can represent their account. This NFT can encode specific
attributes, permissions, or properties related to the user, such as staking
rights, access to certain functionalities, or governance privileges within a
decentralized ecosystem. In particular, the use case of proxy-staking accounts
leverages this NFT-based approach for staking mechanisms. Instead of the
conventional method of staking tokens in a wallet, users stake their NFT-based
accounts’ tokens. The NFT encapsulates staking parameters, delegation
preferences, and other relevant details for participating in a proof-of-stake
(PoS) or delegated proof-of-stake (DPoS) consensus mechanism. Through this
model, the NFT serves as a representation of ownership and a means to
determine the user’s staking weight and influence within the network. The more
tokens staked through a bound NFT account, the more significant the user’s
impact on consensus, rewards, and potentially, governance decisions.

Furthermore, NFTAA can facilitate delegation strategies, allowing users to
delegate their staking rights or influence to other accounts or entities while
still maintaining ownership of their NFT-based account. This flexibility
enhances the overall decentralization and participation in the network. This
proposed framework does not emphasize the preservation of backward
compatibility with existing NFT contracts, abstaining from alterations to the
ERC-721 standard. However, it is theoretically possible to choose the standard
to be used when creating NFTAA so that we could use ERC-165, but of course, we
prefer to use ERC-721. Alternatively, a partial subset of the ERC-721
interface could be used (e.g., ENS NameWrapper names).

###  IV-C NFTAA vs TBA

As highlighted in Section III-D, EIP 6551 presents certain limitations. Our
solution, however, does not prioritize connecting existing NFTs but enables
bidirectional binding of the NFT and Proxy contract. Consequently, upon
ownership of an NFT, we can discern from the NFT metadata that it is
associated with another smart contract, indicating its status as an NFTAA.
Furthermore, we enhance transparency by ensuring the atomic creation of the
NFT and proxy contract within a single transaction, thereby promoting seamless
integration. Likewise, our design does not need the registrar service to
create the TBA address as opposed to TBA. In our case, the factory contract
creates the NFTAA contract with functionality that also works as the NFTAA
address (TBA uses one more address than NFTAA). Another difference is that in
TBA, you could have more accounts on one NFT, which in our case is not
possible due to the atomic creation of exactly one NFT at the time of creating
the NFTAA smart contract (we first create the account contract and exactly
after that the unique NFT). However, theoretically, we could use already
existing NFTAA as the NFT in TBA :-). Regarding security, there are at least
two differences between NFTAA and TBA. The first is the possibility of
generating the address of TBA sooner without having the deployed contract (as
the create2 function for creating contracts is deterministic, i.e., you can
calculate the future contract address). In this case, if the upcoming smart
contract is badly developed (does not contain an execute function for byte
calls to other contracts) or is not upgradeable, it can happen that assets or
liquidity sent to the TBA will not be withdrawable and become locked forever
(even the NFT bounded in TBA can be sent by a mistake (if not safeguarded) to
the address of TBA. Therefore you lock yourself from it). The problem is that
TBA uses only the address of any contract you want in the registry contract
and does not look for any details on how the contract looks or if it is
already deployed. In our case, the account form is pre-defined in the factory
contract, and even after deployment, we guarantee upgradeability as it is a
proxy account. The second security issue is potential fraud, which is
described in the EIP 6551 specification
111https://eips.ethereum.org/EIPS/eip-6551#fraud-prevention that you withdraw
assets from the TBA and at the same time sell the NFT to someone who fought
that they will also have the assets in the TBA. In our case, we provide the
security measures for not withdrawing the assets from the NFTAA while also
selling the NFT, which is bound to the NFTAA smart contract. A small
difference is also in the address where you receive the assets (unstake in the
case of staking). In TBA, the unstaked amount will go to the TBA address; in
NFTAA, the unstaked amount will go to the NFTAA smart contract address.

##  V Evaluation and testing

When testing decentralized applications, the most important thing to focus on
is the core functionality performed on the blockchain. The most significant
part is the smart contract. Testing smart contracts is more complicated than
testing regular software, but many tools make this easier nowadays. One of
them is the Ethereum development environment Hardhat [20]. This development
tool allows us to run the blockchain network locally and, among other things,
provides extensive support for testing and mocking data to simulate a real
blockchain environment. We provide the source codes on
GitHub222https://github.com/fiit-ba/NFTAA.

###  V-A Smart contract testing

Based on these functionalities, we built our tests documented in Figure 4. The
tests were built to evaluate the key elements of our concept. To this end, the
tests mainly focus on:

  * •

Flow test - determine whether the system can successfully mint a new NFTAA
contract, emit a ’NewNFTAA’ event, and check if the minted NFT is bonded.

  * •

Validations - the system ensures that transactions attempting to mint an NFTAA
contract with an empty or excessively large description are correctly
reverted.

  * •

Staking - ensures that users can stake their funds, increase their stakes, and
unstake them. Additionally, it verifies that users cannot unstake before the
system reaches the unlock time.

  * •

Attributes - the system’s ability to return the proper bound NFT ID and NFTAA
note is tested in these tests.

  * •

Proxy - examine if the system correctly revokes actions taken by parties other
than the contract owner and whether it issues a ”ProxyResponse” event whenever
a legitimate function call performed via the proxy is received.

Figure 4: Results of smart contracts testing

Eleven subtests passed the testing phase. By running these automated tests, we
can ensure that the smart contract system performs as expected and adheres to
our expectations.

###  V-B Requirements evaluation

The evaluation of requirements, as depicted in Table I, demonstrates the
successful implementation of key features within the system. The initial
requirement (Request 1.) ensuring users can connect their wallets has been
met, establishing a fundamental connection between users and the platform.
Subsequently, the creation of NFTAAs (Non-Fungible Token Asset Accounts) is
confirmed successful (Request 2.), emphasizing the system’s capability to
generate unique and distinct token accounts. Transactions are seamlessly
facilitated with the successful transfer of NFTAAs between wallets (Request
3.), affirming the platform’s robustness in handling asset transfers.
Stakeholder engagement is supported through functionalities such as staking
(Request 4.) and unstaking (Request 5.) via NFTAA, reflecting the system’s
commitment to user participation in blockchain-based activities. Moreover,
users can conveniently monitor their NFTAAs (Request 6.), fostering
transparency and awareness of individual token holdings. The system’s ability
to verify ownership of NFTAA (Request 7.) adds an additional layer of security
and accountability. The rest of the requirements are non-functional. We did a
thorough, smart contract security audit by tools
Slither333https://github.com/crytic/slither and MythX444https://mythx.io/ to
evaluate non-functional requirement number fourteen. There were no critical or
severe issues in the security model. As a result, the acceptance testing of
the non-functional requirements is successful. The evaluation underscores the
system’s effective incorporation of essential functionalities, meeting or
exceeding the specified requirements and providing users with a comprehensive
and reliable blockchain experience.

TABLE I: Evaluation of requirements

Request identifier | Description of the requirement | Evaluation
---|---|---
1. | The system shall allow users to connect their wallet | Successful
2. | The system shall allow users to create an NFTAA | Successful
3. |  | The system shall allow users to transfer NFTAA
---
to another wallet
Successful
4. | The system shall allow users to do stake via NFTAA | Successful
5. | The system shall allow users to do unstake via NFTAA | Successful
6. | The system shall allow users to check their NFTAAs | Successful
7. |  | The system shall allow users to check
---
owner of some NFTAA
Successful
8. | The system core functionality shall be implemented by smart contract | Successful
9. |  | The system shall provide a user-friendly interface, with clear and
---
concise instructions and error messages
Successful
10. |  | The system shall be scalable to handle a large number of users
---
and data storage requirements
Successful
11. | The system shall be used by any wallet | Successful
12. | The system shall be compatible with modern web browsers | Successful
13. |  | The system shall be compliant with relevant industry standards
---
and best practices
Successful
14. | The system shall be secure and protected against cyber-attacks | Successful

##  VI Conclusion and future work

Non-fungible tokens as accounts have massive potential in the Ethereum
ecosystem. They can provide a valuable asset that can be used as an account in
the runtime and traded on the market. One of the best features of the NFTAA
system is that any account type can cooperate with NFTAA: externally owned
accounts, smart contracts, proxies, or multi-signature accounts. Staking is an
excellent use case example for NFTAA. Unlike classic liquid staking, NFTAA
does not rely on any DAO, multi-signature accounts, or entity that manages the
token; instead, the owners are in full custody of their assets. Additionally,
the network does not lose any security since no funds are unstaked and can be
withdrawn. Moreover, non-fungible tokens can be used in other DeFi
applications, such as lending, borrowing, and derivatives, so they do not lose
any flexibility. From the implementation perspective, the NFTAA can be
implemented with current and available Solidity tooling. However, the
applicability of NFTAA is not only in staking use case but also company
owning, asset and portfolio management, delegation of rights to another
wallet, DAO governance, or even identity and role management (e.g., you could
have a game profile or persona linked to the NFT and in future sell it with
every item in the itinerary). The possibilities of NFTAA are nearly endless.
However, the key focus area of this research was the area of staking. We are
opening new business opportunities with the new data availability layers and
their re-staking mechanism.

Our solution architecture is designed to be used with layer two solutions that
are an alternative way of expanding Ethereum scalability. Our assessment shows
feasibility and scale in the current Ethereum ecosystem, with a commitment to
address scale concerns more in-depth in future revisions.

In summary, non-fungible tokens as accounts, specifically in the context of
proxy-staking or token-bound accounts, introduce a paradigm shift in account
management and staking within blockchain ecosystems. Integrating unique NFTs
with account functionalities enhances personalization, participation, and
governance within decentralized networks. It reflects the evolving landscape
of blockchain technology, where innovative applications continually redefine
the boundaries of traditional concepts. This paper offers design and
architecture decisions with a simple implementation, which allows developers
and researchers to choose the best solution for their needs.

Future work includes examining other use cases for NFTAA and, most
importantly, conducting a detailed security assessment to identify and
mitigate potential risks. We know that staking through NFTAA reduces asset
loss and network security risks compared to externally owned accounts. By
decoupling the stake from the owner, we make staking delegation more effective
because of the fact that NFTAA serves as a proxy for externally owned
accounts.

Moreover, we would like to observe the usage of NFTAA in different networks,
e.g., the Polkadot ecosystem, where there is already an implementation of
proxy accounts and the unstacking lasts 28 days. Implementing NFTAA in the
Substrase environment means bringing this concept to a completely different
technology. Also, the plan is to extend the research to more enterprise use
cases with great potential for business and blockchain fusion.

## Acknowledgment

This work was supported by the Slovak Research and Development Agency under
Contract no. APVV-20-0338.

## References

  * [1] Elie Kapengut and Bruce Mizrach  “An Event Study of the Ethereum Transition to Proof-of-Stake”  In _SSRN Electronic Journal_ Elsevier BV, 2022  DOI: 10.2139/ssrn.4247091
  * [2] Christophe Schinckus, Canh Phuc Nguyen and Felicia Hui Ling Chong  “Cryptocurrencies’ hashrate and electricity consumption: evidence from mining activities”  In _Studies in Economics and Finance_ 39.3 Emerald Group Holdings Ltd., 2022, pp. 524–546  DOI: 10.1108/SEF-08-2021-0342
  * [3] Benjamin Johnson et al.  “Game-theoretic analysis of DDoS attacks against bitcoin mining pools”  In _Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)_ 8438 Springer Verlag, 2014, pp. 72–86  DOI: 10.1007/978-3-662-44774-1˙6
  * [4] Fahad Saleh  “Blockchain without Waste: Proof-of-Stake”  In _The Review of Financial Studies_ 34 Oxford Academic, 2021, pp. 1156–1190  DOI: 10.1093/RFS/HHAA075
  * [5] Elie Kapengut and Bruce Mizrach  “An Event Study of the Ethereum Transition to Proof-of-Stake”  In _SSRN Electronic Journal_ Elsevier BV, 2022  DOI: 10.48550/arxiv.2210.13655
  * [6] Margaux Nijkerk  “Ethereum Validators Forced to Wait Days to Unstake Amid Celsius Withdraws” Section: Technology, 2024  URL: https://www.coindesk.com/tech/2024/01/05/ethereum-validators-forced-to-wait-days-to-unstake-amid-celsius-withdraws/
  * [7] CJ  “What are Liquid Staking Derivatives (LSDs) and How Do They Unlock Liquidity?”  URL: https://www.coingecko.com/learn/what-is-liquid-staking-liquid-staked-derivatives-you-need-to-know
  * [8] Lido  “What is Lido”  URL: https://docs.lido.fi/
  * [9] Rocket Pool  “Explainer Series”  URL: https://docs.rocketpool.net/overview/explainer-series.html
  * [10] Jayden Windle et al.  “ERC-6551: Non-fungible Token Bound Accounts”  URL: https://eips.ethereum.org/EIPS/eip-6551#example-account-implementation
  * [11] John Isige  “ERC-6551: The Future Token Standard for NFTs and Gaming?”  URL: https://www.techopedia.com/erc-6551-the-future-token-standard-for-nfts-and-gaming
  * [12] Ivan Cryptoslav  “What Is ERC-6551? Explaining the New NFT Token Standard”  URL: https://coinmarketcap.com/academy/article/what-is-erc-6551
  * [13] Ethereum Foundation  “UPGRADING SMART CONTRACTS”, 2023  URL: https://ethereum.org/en/developers/docs/smart-contracts/upgrading/
  * [14] OpenZeppelin  “Proxies”, 2023  URL: https://docs.openzeppelin.com/contracts/4.x/api/proxy
  * [15] Wonseok Choi, Jongsoo Woo and James Won-Ki Hong  “Gas cost analysis of fractional NFT on the ethereum blockchain”  In _2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)_ , 2023, pp. 1–6  IEEE
  * [16] EigenLayer Team  “EigenLayer: The Restaking Collective”  In _White paper_ , 2024, pp. 1–19
  * [17] Branislav Hozza, Viki Val, Adam Prisenžňák and Dusan Morhac  “Sub-scaffold”  URL: https://github.com/kodadot/sub-scaffold
  * [18] Talisman  “Joining EVM Networks”, 2023  URL: https://docs.talisman.xyz/talisman/navigating-the-paraverse/ethereum-features/joining-evm-networks
  * [19] Talisman  “Talisman FAQ”, 2023  URL: https://docs.talisman.xyz/talisman/help-and-support/faq#q-can-i-use-talisman-extension-to-send-funds-to-an-evm-address
  * [20] Nomic Foundation  “Hardhat”  URL: https://hardhat.org/


##### Contributions.

In the present paper, we have laid the groundwork for a general and uniform
theory of transfer of generalized Sahlqvist correspondence and canonicity from
normal BAE-logics to normal DLE-logics. Towards this goal, we have introduced
a unifying template for GMT translations, of which the GMT translations in the
literature can be recognized as instances. We have proved that generalized
Sahlqvist correspondence transfers for all DLE-logics, while generalized
Sahlqvist canonicity transfers for the more restricted setting of bHAE-logics.
The formulation of these results has been made possible by the recent
introduction of a general mechanism for identifying Sahlqvist and inductive
classes for any normal DLE-signature [17]. Consequently, there are not many
transfer results in the literature to which these results can be compared, the
only exceptions being the transfer of Sahlqvist correspondence for DML-
inequalities of [32, Theorem 3.7], and the transfer of canonicity in the form
of d-persistence for intuitionistic modal formulas of [68, Theorem 12]. The
transfer of correspondence shown in this paper generalizes [32, Theorem 3.7]
both as regards the setting (from DML to general normal DLE-logics) and the
scope (from Sahlqvist to inductive inequalities). As discussed in Remark 31,
the transfer of canonicity shown in the present paper is neither subsumed by,
nor does it subsume [68, Theorem 12].

Regarding insights, we have also gained a better understanding of the nature
of the difficulties in the transfer of (generalized) Sahlqvist canonicity via
GMT translations. These difficulties were discussed as follows in the
conclusions of [32]:

> […] a reduction to the classical result for canonicity seems to be much
> harder than for correspondence, due to the following reason. In the
> correspondence case, where we are working with perfect DMAs, there is an
> obvious way to connect with Boolean algebras with operators, namely by
> taking the (Boolean) complex algebra of the dual frame. In the canonicity
> case however, we would need to embed arbitrary DMAs into BAOs in a way that
> would interact nicely with taking canonical extensions, and we do not see a
> natural, general way for doing so.

Our analysis shows that, actually, the problem does not lie in the interaction
between the embedding and the canonical extensions, but rather in the fact
that the embedding $e:\mathbb{A}\hookrightarrow\mathbb{B}$ of an arbitrary DLE
into a suitable BAE lacks the required adjoint maps, and that while the role
of these adjoints can be played to a certain extent by the adjoints of
$e^{\delta}:\mathbb{A}^{\delta}\hookrightarrow\mathbb{B}^{\delta}$ (cf.
Proposition 33), we would need to develop a much stronger theory of algebraic
(generalized) Sahlqvist canonicity in the BAE setting to be able to reduce
(generalized) Sahlqvist canonicity for DLEs to the Boolean setting.

##### Further directions.

As mentioned above, our analysis suggests a way to obtain the transfer of
generalized Sahlqvist canonicity for arbitrary DLE-logics, namely to develop a
generalized canonicity theory in the setting of BAEs which relies on the
order-theoretic properties of maps $\mathbb{A}\to\mathbb{B}^{\delta}$. The way
to this theory has already been paved in [52], where a generalization of the
standard theory of canonical extensions of maps is developed, accounting for
maps $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}^{\delta}$ such that the value of
$f^{\mathbb{A}}$ is not restricted to clopen elements in $\mathbb{B}$.

##### Blok-Esakia theorem for DLE-logics.

The uniform perspective on GMT translations developed in this paper can
perhaps be useful to systematically explore the possible variants of the
notion of ‘modal companion’ of a given intuitionistic modal logic, and extend
the Blok-Esakia theorem uniformly to DLE-logics.

##### Methodology: generalization through algebras via duality.

The generalized canonicity-via-translation result for the bi-intuitionistic
setting comes from embracing the full extent of the algebraic analysis.
Specifically, canonicity-via-translation hinges upon the fact that the
interplay of persistent and non-persistent valuations on frames can be
understood and reformulated in terms of an adjunction situation between two
complex algebras of the same frame. In its turn, this adjunction situation
generalizes to arbitrary algebras. The same modus operandi, which achieves
generalization through algebras via duality, has been fruitfully employed by
some of the authors also for very different purposes, such as the definition
of the non-classical counterpart of a given logical framework (cf. [42, 44,
10]).

## References

  * [1] G. Bezhanishvili.  The universal modality, the center of a Heyting algebra, and the Blok-Esakia theorem.  Annals of Pure and Applied Logic, 161(3):253–267, 2009.
  * [2] W. J. Blok.  Varieties of interior algebras.  University of Amsterdam, Department of Mathematics, 1976.
  * [3] A. Chagrov and M. Zakharyashchev.  Modal companions of intermediate propositional logics.  Studia Logica, 51(1):49–82, 1992.
  * [4] A. V. Chagrov and M. Zakharyaschev.  The disjunction property of intermediate propositional logics.  Studia Logica, 50(2):189–216, 1991.
  * [5] W. Conradie and A. Craig.  Canonicity results for mu-calculi: an algorithmic approach.  Journal of Logic and Computation, 27(3):705–748, 2017.
  * [6] W. Conradie, A. Craig, A. Palmigiano, and Z. Zhao.  Constructive canonicity for lattice-based fixed point logics.  In Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings, volume 10388 of Lecture Notes in Computer Science, pages 92–109. Springer, 2017.
  * [7] W. Conradie, Y. Fomatati, A. Palmigiano, and S. Sourabh.  Algorithmic correspondence for intuitionistic modal mu-calculus.  Theoretical Computer Science, 564:30–62, 2015.
  * [8] W. Conradie, S. Frittella, A. Palmigiano, M. Piazzai, A. Tzimoulis, and N. Wijnberg.  Toward an epistemic-logical theory of categorization.  In 16th conference on Theoretical Aspects of Rationality and Knowledge (TARK 2017), volume 251 of Electronic Proceedings in Theoretical Computer Science, pages 170–189.
  * [9] W. Conradie, S. Frittella, A. Palmigiano, M. Piazzai, A. Tzimoulis, and N. Wijnberg.  Categories: How I learned to stop worrying and love two sorts.  In Logic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings, volume 9803 of Lecture Notes in Computer Science, pages 145–164. Springer, 2016.
  * [10] W. Conradie, S. Frittella, A. Palmigiano, and A. Tzimoulis.  Probabilistic epistemic updates on algebras.  In Logic, Rationality, and Interaction, volume 9394 of Lecture Notes in Computer Science, pages 64–76. Springer, 2015.
  * [11] W. Conradie, S. Ghilardi, and A. Palmigiano.  Unified correspondence.  In A. Baltag and S. Smets, editors, Johan van Benthem on Logic and Information Dynamics, volume 5 of Outstanding Contributions to Logic, pages 933–975. Springer International Publishing, 2014.
  * [12] W. Conradie and V. Goranko.  Algorithmic correspondence and completeness in modal logic IV: Semantic extensions of SQEMA.  Journal of Applied Non-Classical Logics, 18(2-3):175–211, 2008\.
  * [13] W. Conradie, V. Goranko, and D. Vakarelov.  Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA.  Logical Methods in Computer Science, 2006.
  * [14] W. Conradie, V. Goranko, and D. Vakarelov.  Algorithmic correspondence and completeness in modal logic. ii. polyadic and hybrid extensions of the algorithm SQEMA.  Journal of Logic and Computation, 16(5):579–612, 2006.
  * [15] W. Conradie and A. Palmigiano.  Algorithmic correspondence and canonicity for distributive modal logic.  Annals of Pure and Applied Logic, 163(3):338 – 376, 2012.
  * [16] W. Conradie and A. Palmigiano.  Constructive canonicity of inductive inequalities.  Submitted. ArXiv preprint 1603.08341.
  * [17] W. Conradie and A. Palmigiano.  Algorithmic correspondence and canonicity for non-distributive logics.  Submitted. ArXiv preprint 1603.08515.
  * [18] W. Conradie, A. Palmigiano, and S. Sourabh.  Algebraic modal correspondence: Sahlqvist and beyond.  Journal of Logical and Algebraic Methods in Programming, 91:60–84, 2017. doi: 10.1016/j.jlamp.2016.10.006. ArXiv preprint 1606.06881.
  * [19] W. Conradie, A. Palmigiano, S. Sourabh, and Z. Zhao.  Canonicity and relativized canonicity via pseudo-correspondence: an application of ALBA.  Submitted. ArXiv preprint 1511.04271.
  * [20] W. Conradie and C. Robinson.  On Sahlqvist theory for hybrid logic.  Journal of Logic and Computation, 27(3):867–900, 2015. doi: 10.1093/logcom/exv045.
  * [21] B. Davey and H. Priestley.  Introduction to Lattices and Order.  Cambridge University Press, 2002.
  * [22] M. de Rijke and Y. Venema.  Sahlqvist’s theorem for Boolean algebras with operators with an application to cylindric algebras.  Studia Logica, 54(1):61–78, 1995.
  * [23] M. A. E. Dummett and E. J. Lemmon.  Modal logics between S4 and S5.  Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 5(14-24):250–264, 1959.
  * [24] J. M. Dunn.  Positive modal logic.  Studia Logica, 55(2):301–317, 1995.
  * [25] M. Dunn, M. Gehrke, and A. Palmigiano.  Canonical extensions and relational completeness of some substructural logics.  Journal of Symbolic Logic, 70(3):713–740, 2005.
  * [26] L. Esakia.  The problem of dualism in the intuitionistic logic and Browerian lattices.  The Fifth International Congress of Logic, Methodology and Philosophy of Science, pages 7–8, 1975.
  * [27] L. Esakia.  On modal companions of superintuitionistic logics.  In VII Soviet Symposium on Logic (Kiev, 1976), pages 135–136, 1976\.
  * [28] G. Fischer Servi.  On modal logic with an intuitionistic base.  Studia Logica, 36(3):141–149, 1977.
  * [29] S. Frittella, A. Palmigiano, and L. Santocanale.  Dual characterizations for finite lattices via correspondence theory for monotone modal logic.  Journal of Logic and Computation, 27(3):639–678, 2017.
  * [30] M. Gehrke.  Generalized Kripke frames.  Studia Logica, 84(2):241–275, 2006.
  * [31] M. Gehrke and J. Harding.  Bounded lattice expansions.  Journal of Algebra, 238(1):345–371, 2001.
  * [32] M. Gehrke, H. Nagahashi, and Y. Venema.  A Sahlqvist theorem for distributive modal logic.  Annals of Pure and Applied Logic, 131(1-3):65–102, 2005.
  * [33] M. Gehrke and H. Priestley.  Canonical extensions of double quasioperator algebras: an algebraic perspective on duality for certain algebras with binary operations.  Journal of Pure and Applied Algebra, 209(1):269–290, 2007.
  * [34] K. Gödel.  Eine interpretation des intnitionistischen aussagenkalkuls.  Ergebnisse eines mathematischen Kolloquiums, 6:39–40, 1933\.
  * [35] V. Goranko and D. Vakarelov.  Sahlqvist formulas unleashed in polyadic modal languages.  Advances in Modal Logic, 3:221–240, 2000.
  * [36] V. Goranko and D. Vakarelov.  Elementary canonical formulae: Extending Sahlqvist’s theorem.  Annals of Pure and Applied Logic, 141(1-2):180–217, 2006.
  * [37] R. Goré.  Dual intuitionistic logic revisited.  In TABLEAUX, pages 252–267. Springer, 2000.
  * [38] G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, and Z. Zhao.  Unified correspondence as a proof-theoretic tool.  Journal of Logic and Computation, 2016, doi: 10.1093/logcom/exw022 ArXiv preprint 1603.08204.
  * [39] A. Grzegorczyk.  Some relational systems and the associated topological spaces.  Fundamenta Mathematicae, 60:223–231, 1967.
  * [40] B. Jónsson.  On the canonicity of Sahlqvist identities.  Studia Logica, 53:473–491, 1994.
  * [41] N. Kurtonina.  Categorical inference and modal logic.  Journal of Logic, Language, and Information, 7, 1998.
  * [42] A. Kurz and A. Palmigiano.  Epistemic updates on algebras.  Logical Methods in Computer Science, 9(4), 2013.
  * [43] C. le Roux.  Correspondence theory in many-valued modal logics.  Master’s thesis, University of Johannesburg, South Africa, 2016.
  * [44] M. Ma, A. Palmigiano, and M. Sadrzadeh.  Algebraic semantics and model completeness for intuitionistic public announcement logic.  Annals of Pure and Applied Logic, 165(4):963–995, 2014.
  * [45] M. Ma and Z. Zhao.  Unified correspondence and proof theory for strict implication.  Journal of Logic and Computation, 27(3):921–960, 2017.
  * [46] L. L. Maksimova and V. V. Rybakov.  A lattice of normal modal logics.  Algebra and Logic, 13(2):105–122, 1974.
  * [47] J. C. McKinsey and A. Tarski.  On closed elements in closure algebras.  Annals of Mathematics, pages 122–162, 1946.
  * [48] J. C. McKinsey and A. Tarski.  Some theorems about the sentential calculi of lewis and heyting.  The journal of symbolic logic, 13(1):1–15, 1948.
  * [49] J. C. C. McKinsey and A. Tarski.  The algebra of topology.  Annals of mathematics, pages 141–191, 1944.
  * [50] J. C. C. McKinsey and A. Tarski.  Some theorems about the sentential calculi of Lewis and Heyting.  The Journal of Symbolic Logic, 13(1):1–15, 1948.
  * [51] H. J. Ohlbach and R. A. Schmidt.  Functional translation and second-order frame properties of modal logics.  Journal of Logic and Computation, 7(5):581–603, 1997.
  * [52] A. Palmigiano, S. Sourabh, and Z. Zhao.  Jónsson-style canonicity for ALBA-inequalities.  Journal of Logic and Computation, 27(3):817–865, 2017.
  * [53] A. Palmigiano, S. Sourabh, and Z. Zhao.  Sahlqvist theory for impossible worlds.  Journal of Logic and Computation, 27(3):775–816, 2017.
  * [54] A. Prior.  Time and Modality.  John Locke Lectures, 1955-6. Greenwood Press, 1955.
  * [55] C. Rauszer.  A formalization of the propositional calculus of hb logic.  Studia Logica, 33(1):23–34, 1974.
  * [56] C. Rauszer.  Semi-boolean algebras and their applications to intuitionistic logic with dual operations.  Fundamenta Mathematicae, 83(3):219–249, 1974.
  * [57] C. Rauszer and C. Rauszer.  An algebraic and Kripke-style approach to a certain extension of intuitionistic logic.  Panstwowe Wydawnictwo Naukowe, 1980.
  * [58] H. Sahlqvist.  Completeness and correspondence in the first and second order semantics for modal logic.  In S. Kanger, editor, Studies in Logic and the Foundations of Mathematics, volume 82, pages 110–143. North-Holland, Amsterdam, 1975.
  * [59] G. Sambin and V. Vaccaro.  A new proof of Sahlqvist’s theorem on modal definability and completeness.  Journal of Symbolic Logic, 54(3):992–999, 1989.
  * [60] V. Sofronie-Stokkermans.  Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics i.  Studia Logica, 64(1):93–132, 2000.
  * [61] B. ten Cate, M. Marx, and J. P. Viana.  Hybrid logics with Sahlqvist axioms.  Logic Journal of the IGPL, (3):293–300, 2006.
  * [62] J. van Benthem.  Modal reduction principles.  Journal of Symbolic Logic, 41(2):301–312, 06 1976.
  * [63] J. van Benthem.  Modal frame correspondences and fixed-points.  Studia Logica, 83(1-3):133–155, 2006.
  * [64] J. van Benthem, N. Bezhanishvili, and I. Hodkinson.  Sahlqvist correspondence for modal mu-calculus.  Studia Logica, 100(1-2):31–60, 2012.
  * [65] J. van Benthem, N. Bezhanishvili, and W. Holliday.  A bimodal perspective on possibility semantics.  ILLC Publications, Prepublication (PP) Series PP-2016-04, University of Amsterdam, 2016.
  * [66] F. Wolter.  On logics with coimplication.  Journal of Philosophical Logic, 27(4):353–387, 1998.
  * [67] F. Wolter and M. Zakharyaschev.  On the relation between intuitionistic and classical modal logics.  Algebra and Logic, 36:121–125, 1997.
  * [68] F. Wolter and M. Zakharyaschev.  Intuitionistic modal logics as fragments of classical modal logics.  In E. Orlowska, editor, Logic at Work, Essays in honour of Helena Rasiowa, pages 168–186. Springer–Verlag, 1998.
  * [69] F. Wolter and M. Zakharyaschev.  On the blok-esakia theorem.  In Leo Esakia on duality in modal and intuitionistic logics, pages 99–118. Springer, 2014.
  * [70] Z. Zhao.  Algorithmic correspondence and canonicity for possibility semantics.  arXiv preprint arXiv:1612.04957, 2016.
  * [71] Z. Zhao.  Algorithmic sahlqvist preservation for modal compact Hausdorff spaces.  In Proc. International Workshop on Logic, Language, Information, and Computation, volume 10388 of Lecture Notes in Computer Science, pages 387–400. Springer, 2017.