ν-DSI

These notes study how decentralized superintelligence (DSI) and digital tokenomics coordinate work and allocate physical and computational resources among people and agents. The economic mechanisms under study include resource pricing and funding, payment settlement, and rewards for contributions.

We develop formal models, specifications, executable code, and proofs natively in Lean 4. The current examples cover ledger transfers, spending authorization, and payment retries. External protocols provide reference designs for these studies.

Preliminaries #

The preliminaries review reference protocols and define the objects used by the executable examples.

• Modules and interactions: an overview of the environment and the relationships between its parts.
• Quantities and units: shared definitions for energy, time, asset amounts, nonces, and gas fees.
• Blockchain infrastructure: Bitcoin, Ethereum, and Solana: ledger state, transactions, account access, and fees.
• Assets and tokens: stablecoins for pricing and payments, asset identity, and token balances and transfers.
• Wallets and authorization: PASS's wallet model and a concrete spending policy.
• Payment protocols and infrastructure: x402 payment exchange, AP2 authorization, Circle Gateway settlement, and Nevermined metering and billing.
• Agent communication: Agent Cards, skills, interfaces, and task states.

Examples #

• A paid task: authorize a payment of 0.003 ETH, update balances in wei, and return an echo result.
• One paid call: reservation, settlement, refund, conservation of funds, and recovery from a lost reply without a second payment.

Run the example #

Install the toolchain, then run:

git clone https://github.com/CloK-Lab/vdsi.git
cd vdsi
lake build
lake exe demo

The build checks the definitions, examples, and proofs. The demo runs a reservation with settlement or refund, a lost reply followed by a retry, and a payment followed by an echo task.