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 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 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.