Live on Hedera

None of this is a thought experiment. Contracts that Deducible generates have been deployed and exercised on the Hedera testnet, where anyone can inspect what happened.

What has been proven on-chain

A murābaḥah, full lifecycle (the flagship)

The flagship is a cost-plus trust sale. A generated MurabahahGen ran its entire lifecycle on testnet: the bank took possession (qabḍ), disclosed its true cost, concluded the sale at a fixed total, and the customer paid that fixed deferred total. The markup never moved with time, and no late charge could raise the debt. It settled.

contract 0.0.9366104, customer 0.0.9366102,
a fixed total of 1,100,000 tinybar (cost 1,000,000 plus a fixed markup of 100,000),
the sequence acquire → disclose → sell → pay, ending settled = true.

Verify contract 0.0.9366104 on HashScan →

A diminishing partnership, run live

A generated MusharakahMutanaqisahGen ran a full lifecycle on testnet: funding, rent, and a buyout that moved the financier’s share from 8000 bps down to 6000 bps, on-chain. When the asset lost value, the loss was carried onto the financier’s share by transfer, not merely emitted as an event. The financier cannot exit whole. Risk-sharing is enforced in money, on the record.

Zakat, to the cent

A zakat-gated MusharakahZakatGen (contract 0.0.9321137) computed and paid its own zakāt al-tijārah:

on a base of 10,000,000 tinybar,
it moved the maslahah fund by exactly 250,000 tinybar, 2.5%, rubʿ al-ʿushr, to the cent,
automatically, with no one trusted to remember;
below niṣāb, zakatDue correctly returned 0.

Verify contract 0.0.9321137 on HashScan →

A zero-trust valuation oracle

The ConsensusValuationOracle takes signed attestations from an independent committee and returns the median within a dispersion band. When agreement falls below quorum, the value is majhūl and the call reverts; gharar is surfaced as a computed quantity rather than a silent assumption. A divergent committee makes fairValue() revert; a convergent one drives a full lifecycle.

Cost & gas (measured)

A ContractCreateFlow is dominated by the bytecode file upload, billed separately from the create and re-paid on every attempt, so a failed deploy is not free.

ContractCreateFlow
  ├─ FileCreate            ~2.2 ℏ
  ├─ N × FileAppend        ~5.3 ℏ each   (N grows with bytecode size)
  └─ ContractCreateInstance ~17 ℏ        (the mirror-node figure is ONLY this last step)

Worked example, MusharakahJaaihahGen, 19,152 bytes of deployed bytecode:

Item	Value
code-deposit gas	`200 × 19152 = 3.83M` → `setGas(4_000_000)` fails `INSUFFICIENT_GAS`; use 6–7M
file upload	FileCreate + 9 FileAppends ≈ 52 ℏ
create (even when it reverts on gas)	~18 ℏ at 4M
budget per attempt	~70–80 ℏ (large contract); ~40 ℏ small (zakat)

Runtime call gas is cheap by comparison:

Call	Gas
`payRent`	34,546
`buyShare`	49,599
`attest`	27,908
`syncValuation`	62,800

Levers to avoid re-burning the ~52 ℏ upload: set gas tight but sufficient (a gas-failed create still pays it), reuse an existing oracle, reuse already-created role accounts. Two notes that bite. msg.value on Hedera is in tinybar (1 ℏ = 1e8 tinybar), not weibar. And the Hedera SDK’s setDefaultMaxTransactionFee truncates via a 32-bit toInt(), so the cap must be ≤ ~21.47 ℏ (use new Hbar(20)). We record these because a proof you cannot reproduce is not a proof.

The standing boundary

The ledger proves execution: that the generated code does what its invariants say. It does not, and cannot, prove that the rules themselves are correct. That remains the work of qualified scholars. See The epistemic boundary.