sophi 0.2.0

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. 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 a mathematical statement:

sum(before) == sum(after)

Alice's 0.5 BTC plus Bob's 50000 USDT before must equal Alice's 50000 USDT plus Bob's 0.5 BTC after. No value created. No value destroyed. The math either holds or it doesn't.

Sophi verifies this off-chain and produces a proof. That proof is then used to settle on Bitcoin, Lightning, or any network — where funds stay under the users' control until the moment of execution.

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 — the conservation law. sum(before) == sum(after). Always verified automatically.

Proof — the output. A portable JSON that any system can consume to coordinate settlement.

Proof output

{
  "status": "valid",
  "rule": "sum(before) == sum(after)",
  "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.

Why not Solidity?

	Sophi	Solidity
Holds funds	Never	Yes
Executes on-chain	No	Yes
Reentrancy attacks possible	No — impossible by design	Yes
Anyone can read it	Yes	Partial
Network independent	Yes	Ethereum only
Formally verifiable	Yes	No

The DAO hack, Wormhole, Ronin — all were possible because smart contracts hold funds and execute arbitrary code. Sophi eliminates both. You cannot write a custodial program in Sophi because the language has no concept of custody.

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.