Certora Formal Verification Proposal

Proposals
1

Formal Verification and Path Coverage Tools for Continuous Security of the Compound Protocol and its dApps

Summary

A proposal for significantly and continuously improving the security of the Compound platform and the dApps built on top of it, by offering our formal verification and path coverage tooling service to the Compound Platform contributors and the Compound Protocol dApp developers. This is a follow-up to our recent work on the Comet protocol with the Compound labs team. The idea is to provide access to the community and educate the community, write formal specifications, and review code changes. This proposal is orthogonal to the Open Zeppelin proposal, which has already been suggested using the Certora prover. This proposal also suggests writing formal correctness rules for the Compound Protocol which will be reviewed by the community and OpenZeppelin. We have already written some formal requirements for Comet and prevented huge security breaches.

This is an update of an earlier unsubmitted proposal discussed in November 2021.

Background

Compound Protocol Security

The Compound Protocol is a fully decentralized system that provides sophisticated tools for accessing liquidity. The protocol’s ongoing management is controlled by a governance protocol that allows external contributions and voting by stakeholders. Such a system opens up the possibility of creating powerful new DeFi protocols built on top of it, without giving up on decentralization.

One of the major risks in managing a complex system of smart contracts is that it is harder to ensure that changes introduced via governance are safe and that they do not break the behavior of the protocol. While those problems are common to every piece of evolving software, decentralization introduces additional risks.

These risks were highlighted by a recent incident in which a bug was introduced in a Compound governance proposal, leading to huge nonrecoverable financial losses. Of course, such bugs are not exclusive to Compound — they have been affecting many DeFi protocols.

Detecting vulnerabilities before they are deployed is difficult because of the lack of good security tools for smart contract development. Smart contract developers often rely on manual auditing to prevent bugs, but audits are not well suited for the setting of ongoing, time-controlled governance proposals. Moreover, even the best auditor can miss critical bugs due to the complexity of the code.

About Certora

Our team consists of 60 experts in smart contract security, formal verification methods, and compilation techniques. 12 of our team members have PhDs in formal verification from top schools in US, Europe, and Israel. We have built a world-class and unique developer tool that seamlessly integrates into CI/CD, allowing continuous verification of contract correctness.

We enable companies to “move fast and break nothing”, taking months off of the time to market, by decreasing code audit time. Our product, the Certora Prover, allows both pre- and post-deployment code verification: it statically analyzes the code before it is deployed but also runs on the EVM bytecode of the deployed contracts. The product verifies code by checking that it obeys high-level semantic rules. For example, a rule could assert that the sum of token balances remains unchanged by all operations that do not mint new tokens. A free demo of the Certora Prover can be found here. The real tool is quite advanced and handles multiple contracts.

Our product is used by the industry’s leading companies (Aave, Balancer, Benqi, Compound Finance, MakerDAO, OpenZeppelin, Sushi, TradeJoe, Bancor, and more) and has prevented more than 100 safety-critical bugs, including 20 “solvency” bugs (a bug in which a user can steal money from the contract). Each bug can lead to tens or even hundreds of millions of dollars in losses. The Certora technology has also uncovered critical security bugs in the Solidity compiler itself and in deployed contracts of major DeFi organizations. We are also the only team that was able to formally verify interesting security properties including preservation of funds.

Certora developed a new language CVL https://docs.certora.com/ for writing code specifications. As part of this project, the Compound Community will get access to the language and the technology (see Offering Section below).

Certora and Compound Relationship

We have been working with the Compound team almost since its inception. Originally, we formally verified the first Price Oracle implementation. Using the Certora Prover tool, we were able to find a subtle bug after the contract completed auditing by Trail of Bits. The part that we did not verify, the MoneyMarket contract, was later found to contain a serious vulnerability in the liquidation function, potentially breaking the protocol’s solvency, allowing an attacker to steal money from the contract. Compound Labs then asked us to help in formally verifying a sophisticated bugfix, whose goal was to block potential exploits. We have written rules for that purpose, successfully showing that no code paths can trigger the exploit.

In addition, we formally verified the V2 version of the protocol, including the MoneyMarket contract. There, we were able to find more bugs in pre-deployment and post-audit. For example, a rule for ETH borrows written by Jared Flatow (VP Engineering) from the Compound team found a mismatch in the computation of accrued interest, that prevented users from fully repaying loans. We have found many more costly bugs in the platform, preventing immense losses and protecting its users, including in the OpenOracle protocol.

In the verification of the Open Oracle framework with the Uniswap based anchor, we have identified a high-risk miscalculation of the prices of cTokens. In addition, we have verified a set of properties for this contract. The full report is available here https://www.certora.com/wp-content/uploads/2022/02/CompoundUniswapAnchoredOpenOracleAug2020.pdf

Certora is currently verifying Comet and already found 10 critical and high severity issues, including increasing assets by self transferring, missing updates of collateral used, missing updates to the supply and borrow rates and more. We have verified approximately 50 rules. The rules show that the system obeys important security properties of the protocol spanning the core logic of the protocol, high-level mathematical properties of operations such as accrue and, important properties of all the public methods including absorbing and buying collateral. This project will be concluded by the end of March, after which a full verification report will be published.

Specific Rules

As described previously, we have been working closely with the Compound core team. However, we are not working with the Compound Platform contributors (those not directly employed by Compound) nor the Compound dApps developers (those developing dApps on top of the Compound Protocol). Recent exploits (such as the claimComp bug discovered in Proposal 62) show that this approach is insufficient; these exploits have caused hundreds of millions of dollars of losses.

Case Study 1: Applying Certora Prover to check Proposal 62

Proposal 62 pertains to parts of the code that were not verified by Certora, but applying simple rules could have identified the bug. For example, the bug would be detected by the following rule:

Rule: maxCompReward

Description: The max COMP reward of a user has an upper limit, based on the current supplyState, borrowState and compAccured.

Claimed COMP should also satisfy other simple properties, and checking these properties could detect and prevent additional bugs. For example:

Rule: noFrontRunningGainOrLoss

Description: The amount of COMP received at a specific state is the same whether or not another user (possible the admin) has performed an operation just before.

Rule: zeroGainOnZeroBlocks

Description: A user with zero borrows can not gain COMP in a single block (for example by using a flash loan).

An executable formalization of the rules detects the bug introduced in Proposal 62, in particular, the rule called maxCompReward triggers a violation.

Case Study 2: A formal rule for Comet integrity of token balance change

Rule: totalCollateralPerAsset

Description: The sum of collateral per asset over all users is equal to total collateral of asset. This rule is also applied to check all public and external methods of the Comet contract.

This important solvency property which can be easily formulated in Certora’s specification language was violated in a version before deployment and shows a critical vulnerability of self transferring.

Rule: balance_change_vs_accrue

Description: Whenever the system’s borrow token balance changes, it changed after accrue was called and the borrow and supply rates are up to date. This rule is also applied to check all public and external methods of the Comet contract.

After 4 minutes of running time, the Certora Prover located inputs violating the rule in two methods in the methods before deployment:

  1. BuyCollateral - thus enabling to buy collateral (at a discount) when there might be enough reserves and therefore should not be allowed

  2. withdrawReseves - thus enabling the governance to withdraw possible more reserves than there should be able to

Proposal: Dev Tools for Smart Contract Correctness

We propose two approaches to significantly increase the confidence in the platform itself and in the smart contracts built on top of it. The first is the Certora Prover, and the second is a new symbolic execution tool (path coverage). Both of these methods leverage the high-level rules to guarantee that all paths of the code satisfy the rule.

The two approaches are complementary: The Certora Prover will prove that specific critical parts of the code are sound and will find hard to detect bugs, while the symbolic execution tool will be running 24/7 to continuously increase the coverage for specifications that are too complex to prove using the Certora Prover.

In the following sections, we will specify the deliverables of our proposal.

Formally Specifying High-Level Rules of dApps in Open-Source CVL

We will carefully review every proposal of a code change by the community and write high-level correctness rules in English and in CVL, Certora’s domain-specific specification language. This includes development for DeFi smart contracts built on top of Compound, as well as for the Compound platform itself via its contributors. These rules will be used later for the Certora Prover and the new path coverage tool. In the unlikely event that a bug is reported, we will generalize the bug and write high-level rules preventing similar bugs to occur in the future.

These engineers are readily available and familiar with the logic of the Compound Protocol. Our current backlog for customers is several months.

Fitting the DeFi community spirit, we will make the CVL rules open-source, allowing decentralized rule writing and rule auditing. This will allow knowledge-sharing in rule writing between contributors and dApp developers, allowing developers to reuse application rules.

We will compensate non-Certora rule writers with COMP tokens according to their contributions.

We will create a forum for community rule writing. Contributors will have access to the Certora platform (including education material and rules from other projects) and the current set of rules.

Every rule suggestion will be reviewed jointly by the Compound labs and the Certora team. The reward will be decided jointly based on the significant contribution.

Formal Verification of Smart Contracts during CI/CD

The above rules will be used by the Certora Prover, which will be available to all Compound platform developers. The CVL will be integrated as part of a VSCode extension, with tooling to integrate CVL specs to the Solidity code project. The extension will also be able to invoke the Certora Prover, and present an ongoing status of the rules: whether they are proven or violated. When a rule is violated, the extension will return a concrete call trace showing the input for which the rule is violated, in a view similar to a debugger.

Code Coverage for Smart Contracts

This project is inspired by the Sage Direct Fuzzing Project which prevented million-dollar bugs for Microsoft.

We will develop a new symbolic execution product for increasing code coverage of the Compound smart contracts. For each smart contract, the product will automatically generate inputs and check that the contract obeys the rule for those inputs. The product will harness SMT solvers to continuously enumerate additional control flow execution paths. The tool can continue to run post deployments and results will be available on a dashboard. This approach complements formal verification when the code is too complex for it or when using it is too computationally intensive. The Kotlin source code developed in this project will be publicly available from June 1st to allow contributions from the community. This includes CVL and its interpreter. The proposed license is https://polyformproject.org/licenses/noncommercial/1.0.0/

This Code Coverage Tool is similar to Dynamic Monitoring provided by Forta, however, our tool is different in two aspects: it uses high-level security rules and leverages SMT solvers for triggering rarely executed scenarios.

In addition to creating the product, we will create a dashboard that will report the inputs and the paths covered by the different inputs, as well as rule violations that may occur. Also, for each input, we check and report that every CVL rule holds.

Measures of Success

In general, we note that there is no silver bullet in smart contract security and in formal verification specifically. Still, we plan to measure success according to the following measures: (1) the number of paths covered by the path coverage tool, (2) the number of rules formally proved, (3) the number of bugs identified by the Certora Prover before deployment, (4) the number of bugs identified by the path coverage tool, and (5) the number of missed bugs in code analyzed by Certora found by auditors and other means. The numbers will be available on a daily basis.

The Certora Prover takes a Solidity contract and a CVL specification as input and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of Certora Prover are scoped to the provided specification, and cases that are not covered by the specification are currently not checked by Certora Prover.

Certora Services Summary

We offer the following services by the company:

  • We will create a two-week online course on writing rules designated to the Compound Protocol. The course will be recorded for availability for all developers.
  • We will hold as many as needed Zoom calls for users of the Certora Prover and the new path coverage tool whose source is available using the Polyform License.
  • The Certora team will create a shadow git repository for the Kotlin code. Anybody in the Compound Community can get limited and revocable access to the repository against a signed NDA. We will allocate up to 20 keys to DApp developers accessing our SaaS platform with unlimited compute usage. Computation time will be billed to Certora. Additional keys are available for $4000/month as approved by the Compound ecosystem.
  • We will allocate a team of two R&D personnel to write rules for up to 8 weeks per year. Additional weeks will be available subject to charge and availability. We will offer a 30% reduction on the normal professional service prices.
  • We will create a dashboard displaying the results of the path coverage product, including rule verified and covered paths, visible to all Compound users. Rule violations will be reported automatically to the Compound security team, but not visible to all users to avoid revealing potential exploits.
  • We will create an open-source database of CVL rules and the code they refer to, to decentralize rule writing and promote decentralized contributions to rules.

Price

  • The annual price is $2,000,000. $1,000,000 is paid in USDC. $1,000,000 is paid in COMP tokens.
  • An additional sum of $400,000 in COMP paying decentralized community rule writers. This sum will not be used for any other purpose and returned if not used or moved to the following year if the contract is renewed. These tokens will be transferred to a special-purpose multisig wallet controlled by Certora and elected members of the Compound ecosystem
9 Likes
2

Thanks Shelly for renewing the discussion around continuous formal verification. I personally would like to see something like this adopted by the protocol as soon as possible, as formal verification with Certora has indeed been an important part of the quality assurance process we use for smart contract development at Compound Labs. I would very much like to see the community adopt a similar practice around all potential modifications to the protocol. I think the exercise of trying to articulate invariants about code being added or changed in itself helps increase the security of the protocol significantly, let alone the actual corner and counter cases discovered by running specific rules.

Certora is offering to help write rules, to teach the community how to write rules, and to run the rules on their servers. They are also offering to make their source code available to the community, which is something they have never done before. This means that Compound protocol developers would be able to run formal verification locally, understand what it’s doing, and potentially diagnose or patch any issues they may encounter. I think this is an important consideration for adopting such a new technology, and am really glad to see Certora moving in this direction. This is hopefully a step in the direction of them completely open-sourcing the technology, which is something I think would give the community a lot of confidence that investing into CVLs will have a minimum long-term value for the protocol. I also think it aligns with the spirit of development for the Compound protocol and decentralized finance overall.

In my opinion, continuous formal verification is a step towards more efficient governance. It would decrease risk for the protocol and give further insight to governance, which can inform decision making. It should be part of our complete strategy for maintaining the integrity of the protocol, and this proposal gets us a long way towards those goals.

6 Likes
3

Gauntlet is supportive of Certora’s formal verification proposal. As the Compound community continues to innovate via governance, it is paramount that protocol changes do not introduce security risks to the Compound ecosystem. Continuous formal verification can drive quality assurance and help prevent damaging security breaches, so we view formal verification and path coverage tools as highly valuable for decentralized governance.

One question @Shelly : can you provide more detail on how Certora will help ensure that Asset Listings to the protocol do not introduce security risks? The community has been focused on adding new assets to the protocol to further diversify and strengthen the Compound ecosystem.

2 Likes
4

Hi Paul and thanks for your feedback.

Certora’s rules match an interface. Therefore, once written for a contract like an ERC20 token or a cTokenm, they can be executed on any implementation of the interface.

Certora has written a spec for some basic properties of a cToken. We plan to extend it to cover more properties of the listed assets, and to write ERC20 properties that address the specific assumptions of Compound’s system.

2 Likes
5

Such services are helpful to Protocol, just for the user to choose to use Compound, it adds a little more trust.But the expense is disproportionate to the corresponding benefit.

Actually, This kind of service is useless, the protocol will not become more secure because it has passed formal verification, and formal verification will not be responsible for security incidents.

OpenZeppelin is already doing well, Certora worked with Compound early, but failed to prevent the bugs produced by Proposal 62,Is it because Compound didn’t pay for the partnership service before?

Supporters are willing to pay up to 2M(6% of Protocol’s annual revenue) for these services, but Compound’s highest bounty in immunefi is only 50k. The successful case of immunefi is more cost-effective than certora. At least the fees paid at immunefi are guaranteed to solve some problems.

2 Likes
6

This was posted by Michael George yesterday.

Thank you for your reply. I think your questions indicate a few misconceptions about the proposal that would be helpful to clear up.

Certora’s previous work with Compound only covered the core protocol; we did not verify governance proposals. Above we described a rule that would have detected the bug in Proposal 62, but we wrote this rule after-the-fact to show that Certora’s technology could have caught the bug. If Compound had been performing continuous verification as outlined in this proposal, it is possible that they would have discovered the bug before Proposal 62 was accepted. The Certora Prover integrates into CI/CD so after every change in the code, similar to regression testing, the rules are re-verified that the new code is still correct

The Certora Prover’s primary purpose is finding bugs during development, rather than proving their absence (although a successful verification also shows that a protocol takes safety and security seriously). It is only possible to produce proof if the protocol being verified actually satisfies its specification - if there are vulnerabilities in the contracts being verified, the Prover will demonstrate those vulnerabilities, allowing the developers to find them and fix them.

The power of the Certora Prover as a bug-finding tool was recently demonstrated by TrustToken’s “red team” review of their security practices. They injected security vulnerabilities to see what security tools were best at catching them. Of the 23 injected bugs, Certora’s Prover found 17 of them, while manual auditing uncovered only 8 of them and bug bounties found only 3. Only 4 vulnerabilities were found by others but missed by the Prover, while 12 vulnerabilities were found by the Prover but missed by others:

image (4)
image (4)1760Ă—932 45.3 KB

Audits and bug bounties are useful and work well with formal verification in the DeFi security toolkit. See Auditing and Formal Verification - Better together. Auditors can review the CVL rules. Whitehackers can insert bugs into the code before it is deployed and see if the current rules suffice. The OpenZeppelin proposal also suggests that the Certora tool will be used.

Open Zeppelin is using Certora to formally verify their governance contract, see the latest verification report.

4 Likes
7

Hello everyone,

As Compound’s Security Advisor, I’d like to clarify a few things around how we, at OpenZeppelin, expect Certora’s Formal Verification Proposal to work within our existing partnership and Compund’s overall security.

Past Discussions of Formal Verification

As we mentioned during the Audit Proposal discussions in November, we see Formal Verification (FV) as a component of an overall holistic security process that must include coding best practices, manual auditing, education, threat monitoring, other testing suites and bug bounties. We have an existing relationship with Certora and are fans of the progress their technology is making but we leave the decision of pricing and vendor selection up to the Compound community. We had previously mentioned the possibility of offering FV security services but that never materialized in our existing proposal since there was no active FV vendor at the time.

Audit Scope for FV Rules

Formal verification is only as good as the initial description of the desired properties of critical elements of the protocol, which is why it is important that FV rules are written correctly. However, given the current scope of our security partnership, OpenZeppelin auditors would not be involved in either writing or reviewing FV rules. We’ve learned how important it is to prioritize auditor time to avoid backlogs on important proposals and reviewing FV rules line-by-line in addition to the code would mean potentially doubling the timeline of any audit engagement on protocol changes.

During our audits, we do often look at tests to understand developer intentions in the code but we do not offer security reviews of the tests themselves and FV rules would be no different in this regard. We would assume that any necessary FV-specific supporting services will be performed separately by the Certora team as part of their proposal.

This all being said, we do think that having robust FV rules would enhance the security of governance proposals and would be a good way to prepare for an audit by catching bugs during development. We already recommend that our audit clients build a robust test suite, which can include FV, as part of their Audit Readiness.

Other Clarifications

There are a few other things we wanted to address from the forum discussion:

  1. Asset Listings - Asset Listing Proposals would certainly be a good use for FV and could cover some of the items in our recent Asset Listing Checklist. However, it’s important to note that not all checks may be possible with FV rules written for Compound on external assets so additional security tooling and manual checks may still be necessary.
  2. Comparison to Forta - @shelly earlier mentioned that Certora’s Code Coverage tool was similar to the Forta Network being used in our monitoring solution for Compound. It’s important to distinguish that Certora’s tooling here is used for evaluating code prior to deployment while Forta is built to monitor live smart contract events after deployment in either the protocol itself or external contracts such as oracles and ERC20 contracts for CToken markets. We see these two tools as entirely separate to be used for different security needs.
  3. Security Decision-maker - Certora makes mention of both Compound Labs and a “Compound security team“ that would be involved in deciding new FV rules and handling payments to community rule-writers. When OpenZeppelin has needed the DAO to make security-related decisions, we’ve defaulted to asking the Guardian Multi-sig but we’re happy to go with Labs or a different entity if that’s preferred by the community. Therefore, we’d like to understand if Certora expects Compound Labs to be the decision-maker in all these instances or if they are expected to fall elsewhere. In any case, it’s important that security decision responsibilities are clearly defined to avoid confusion and potential problems in the future.

Summary

Overall, more security tooling is always a good thing and we’re happy to see discussions on additional ways to protect Compound beyond just security audits, advisory and monitoring. OpenZeppelin’s feedback above is intended to be neutral on Certora’s proposal since we believe this needs to be guided by Compound’s vendor selection process. Our goal here is to clarify some assumptions on how OpenZeppelin’s existing partnership would be impacted and where FV could be used in Compound’s proposal lifecycle. We leave it to Certora and the community to decide how they’d like to proceed.

2 Likes
8

Hi and thank you @cylon for your feedback.

We want to clarify the role of formal verification in the security process. A widespread misconception about formal verification is that it is only useful during development, before an audit. In fact, our tool sometimes finds bugs after audits, and even after the code is deployed.

For example, here are some bugs that we found with our technology after completion of a traditional audit:

To be clear, traditional audits are also an important part of any security process; formal verification does not replace auditing. Rather, FV and audits are complementary techniques that can discover different classes of bugs - both are important.

2 Likes
9

Obviously , spending 2M$/year for FV service is not cost-effective .
As with the proposal to donate to the Nomic Foundation , supporting the development of the Ethereum infrastructure is good , but the expenditure is too large and the community (mostly VCs ) rejects it .
No matter how you describe FV’s effectiveness in Defi contract auditing , OpenZeppelin doesn’t want to increase the workload , and the community has chosen OpenZeppelin .
Let’s make an assumption that the community is only willing to pay Grant about 150k/year , is Certora still willing to provide services ?
If Certora starts to serve Compound for free now , until Certora finds serious security problems and helps the protocol to be patched , the community will propose a corresponding bonus to Certora ?
Can Certora accepts this form of cooperation ?

10

DDoS is a big threat to websites and users,Should I pay a large service fee for CloudFlare regardless of the website is DDoSed or not?

CloudFlare can describe a lot of their cases and strategies to prevent DDOS, you only need to pay for it, and sometimes it is unnecessary.

“Cloudflare’s 121 Tbps network blocks an average of 86 billion threats per day, including some of the largest DDoS attacks in history.”

It is not friendly to pay high service fees in advance,free service and pay for security bugs are more reasonable, or lower service fees.

Of course ,you should be lobbying the head VCs, they control the votes.

11

Our pricing is based on allocating 20 users to the platform. If the community demands more we can increase this. For example, in the Aave grant, we allocated 100 keys.

We are a team of 65 people developing sophisticated software, solving the hardest problem in computer science–statically verifying that the code behaves as expected. Many of us spent 10 years in grad school. It is unfair to compare our price to DDOS protection services.

In addition, we allocate 2 people for 8 weeks to write new security rules. We include unlimited support in this package. This adds an extra layer of security on top of great auditors. We believe that for a protocol holding $6bn in TVL, the cost of a potential hack or failure could be far worse than the costs of extra security.

3 Likes
12

Compound protocol revenue is about 30M/year

image
image1700Ă—632 53.6 KB

$1M a quarter for Gauntlet. $4M/Year

There is no evidence that the optimization of Gauntlet’s parameter tuning has improved capital utilization efficiency or borrowing volume growth for Compound users .

Assuming each parameter adjustment brings in more Borrowing volume, Compound’s borrowing volume should grow, in fact it dropped from 7.8B to 2.4B a year ago.

image
image1700Ă—685 57.7 KB

$1M a quarter for OpenZeppelin. $4M/Year

At present, it has done a good job and optimized the assets listing process.

$0.9M for CompoundGrants.

https://compoundgrants.org/list-of-funded-grants

Nomic Foundation has tried to apply for 16% of the annual revenue for free.

There may be some costs that I don’t know. There’s not much left.

I will not doubt your professional ability and the professional level of your personnel, you must be the top among the enterprises that can provide FV services.

As a security advisor, OpenZeppelin’s reputation will be affected by negligence and hacking incidents, and they will not relax.

If OpenZeppelin missed some major security issue, but then Certora’s FV service found it.

OpenZeppelin should take some responsibility for this, but I think it’s very unlikely to happen, OpenZeppelin has done a good job, and Certora has not found major issues after the OpenZeppelin audit, which is the norm.

Certora provides services first, and Certora finds problems after OpenZeppelin, and it is more appropriate for the community to pay Certora fees each time. This is a better way to cooperate.

Trail of Bits and ChainSecurity may also be able to provide more multiple security services, and they may also find other security issues after the OpenZeppelin and Certora audits.

To maximize security, Compound should buy all security services and audits regardless of expense.

we already have OpenZeppelin and pay $4M/year for it, I don’t think it’s necessary to spend another $2M.

1 Like
13

While I agree that costs all around are too high, I personally think all changes to the protocol should go through some sort of formal verification process first and developers should think through invariants to changes they are making. I think that’s something that the protocol has unquestionably benefitted from and will continue to benefit from. We should re-evaluate all the services and whether the fees should be adjusted, but we shouldn’t sacrifice formal verification just because we are paying too much for other services.

2 Likes
14

Cloudflare: Proof of Stake and our next experiments in web3