winnow

A BITCOIN WALLET FOR IPHONE · WRITTEN IN LEAN 4

Your bitcoin.
Your choice
of control.

Pay from your phone, add a Ledger,
or share a wallet.

Download for iPhone Watch it work

Open source · MIT · TestFlight · iPhone, iPad and Apple silicon Mac

Choose who signs

One key. One decision.

Receive, review, send. All from your phone.

1 key · 1 signature

Two keys. Both sign.

Your phone and a Ledger both approve each payment.

2-of-2 · 2 signatures

Two approve. One can be away.

Any two of three signers can approve a payment. Add a recovery path that opens after a delay.

2-of-3 · 2 signatures
THE ACTUAL APPRECORDED BY CI ON REGTEST
Your everyday wallet in the real Winnow app.
01 / 03Your everyday wallet
Your phone and a Ledger in the real Winnow app.
02 / 03Your phone and a Ledger
Any two of three in the real Winnow app.
03 / 03Any two of three
See the full journey

SEE FOR YOURSELF

One wallet. Three ways to pay.

01 Everyday02 Both keys03 Any two

Real payments on a private regtest node, recorded by CI. The 2-of-3’s other signers are Bitcoin Core wallets on that node; the Ledger is simulated. Recording & source ↗

CHECKED ON EVERY COMMIT

Every change runs the app.

Each change to Winnow builds the app from its Lean source, runs it in a simulator against a private Bitcoin node, and records what happened. The screens above come from the newest run that passed.

Commit
aafda65
Device
iPhone 17 Pro · iOS 26.5
Network
regtest
Recorded
2026-11-14
  • Lean built from source, every proof checked
  • Wallet, network and multisig tests against Bitcoin Core on a private regtest node
  • Simulator and device builds, each checked to contain no Swift
  • Release builds checked to carry no test mode
  • The app driven through these journeys on screen, and recorded

A release tag runs all of it again before a build goes to TestFlight.

  1. An ordinary paymenttestCreateReceiveSendConfirm6 screens26 spassed
  2. Two of three, and the recovery pathtestMultisigTwoOfThreeWithRecovery9 screens1 min 39 spassed
  3. Fee bump replace confirmtestFeeBumpReplaceConfirm2 screens46 spassed
  4. Retry after no peerstestRetryAfterNoPeers1 screen20 spassed
  5. A Ledger as the second keytestLedgerPairVerifySpend6 screens1 min 41 spassed
  6. Ledger card two of twotestLedgerCardTwoOfTwo4 screens21 spassed
  7. The peer censustestShippedCensus6 screens19 spassed
  8. A silent paymenttestSilentPaymentSend2 screens20 spassed
  9. Spent elsewheretestSpentElsewhere0 screens1 min 6 spassed

WRITTEN IN LEAN 4

No Swift. One language, top to bottom.

01 · The wallet

Bitcoin in Lean

Keys, transactions, PSBTs, descriptors, compact-filter sync, peers and broadcast are Lean 4 compiled to C. Every signature runs on a secp256k1 whose arithmetic is proven in Lean.

02 · The app

Model, update, view

Each screen is a Lean function from the wallet’s state. Standard iOS controls draw it, through an Objective-C shell that is itself printed from Lean at build time.

03 · The framework

LeanNative

Keychain, Face ID, Bluetooth, iCloud and background tasks reach Lean as typed capabilities. The Xcode project is generated from a Lean description of the app, which refuses a permission without its explanation.

Source on GitHub ↗How it worksHow the port was checked ↗LeanNative ↗

The wallet, in action.

Private regtest · recorded by CI · Recording provenance