sophi 0.2.2

A simple language for Bitcoin non-custodial smart contracts

Sophi

A simple language for Bitcoin non-custodial smart contracts.

Sophi is not a smart contract language like Solidity. It has no runtime, no blockchain execution, and no custody of funds. You describe what a fair exchange looks like — and Sophi proves it is mathematically valid.

Install

pip install sophi

Write a swap

swap {
  before:
    alice = 0.5 BTC
    bob = 50000 USDT

  after:
    alice = 50000 USDT
    bob = 0.5 BTC
}

Save as trade.sph and run:

sophi compile trade.sph

That's it. Sophi checks that no value was created or destroyed — per asset, per participant. If the math holds, it produces a validity proof. If not, you get a clear error before anything touches a network.

Works for any number of participants

swap {
  before:
    alice = 0.5 BTC
    bob = 50000 USDT
    carol = 1 ETH

  after:
    alice = 50000 USDT
    bob = 1 ETH
    carol = 0.5 BTC
}

2 people, 3, 8, or any number. Sophi handles it automatically.

How it works

Every Sophi program is verified against two mathematical rules:

1. Conservation per asset — the total of each asset before must equal the total after.

BTC before  == BTC after
USDT before == USDT after

This means 1 BTC → 1 USDT is always rejected. BTC is not USDT. Each asset is verified separately.

2. Delta per participant — Sophi calculates exactly what each person gave and received.

alice: -0.5 BTC, +50000 USDT
bob:   +0.5 BTC, -50000 USDT

No value created. No value destroyed. The math either holds or it doesn't.

Proof output

{
  "status": "valid",
  "conservation": {
    "BTC":  { "before": "0.5",   "after": "0.5"   },
    "USDT": { "before": "50000", "after": "50000"  }
  },
  "delta": {
    "alice": { "BTC": "-0.5",  "USDT": "+50000" },
    "bob":   { "BTC": "+0.5",  "USDT": "-50000" }
  },
  "before": { "alice": "0.5 BTC",    "bob": "50000 USDT" },
  "after":  { "alice": "50000 USDT", "bob": "0.5 BTC"    }
}

This proof is portable. Bitcoin, Lightning, your own backend — any system can consume it to coordinate settlement without trusting a third party.

The four primitives

These exist under the hood. You never write them — Sophi infers them from your swap.

Resource — anything with value. BTC, USDT, ETH, or any asset you name.

State — who holds what. before and after are states.

Rule — conservation per asset. Verified automatically for every asset in the swap.

Proof — the output. A portable JSON with conservation, delta, and status.

Non-custodial by construction

Your funds never leave your control. Sophi has no concept of custody. It is mathematically impossible to write a custodial program in Sophi.

Independent from any platform

Sophi is a standalone language. It does not depend on any specific platform, exchange, or settlement system. The proof it produces can be used by anyone.

License

Business Source License 1.1 — converts to Apache 2.0 after 4 years.