What is Deducible?

Deducible is a compliance-by-construction compiler for Islamic-finance contracts. You write the terms of an instrument in a small language called .fiqh; the compiler reads those terms the way a careful jurist would, and either lowers them to a smart contract — or refuses, naming the principle the terms offend.

The point is in that refusal. A contract that disguises a loan as a partnership is not approved, not merely warned about — it will not compile, and no contract is emitted.

The gap it closes

Strip away the vocabulary and Islamic finance rests on one old, sharp distinction:

• A loan returns the lender a guaranteed increase no matter what happens to the borrower. That fixed, risk-free extra is riba — forbidden plainly (al-Baqarah 2:275).
• A partnership ties reward to risk: partners share profit and loss in proportion to their stake (al-ghunm bi-l-ghurm).

On paper you can dress a loan in the costume of a partnership — call it musharakah, then quietly guarantee one partner’s capital back, win or lose. The words say partnership; the behaviour says loan. Scholars call this worry form over substance.

Today, the safeguard against it is attestation: a Shari’ah board reads the contract and signs that it is sound. That is real and valuable work — but it is a promise. You trust that the board read carefully, that the contract they read is the one you signed, and that the one you signed is the logic the bank’s systems actually run, year after year. Somewhere along that chain, substance can quietly drift from form again.

Compliance, today, is promised. It is not proven.

The shift

Deducible moves the guarantee from attestation to construction. Instead of catching a bad contract after the fact, it makes the bad contract impossible to express — the way you cannot draw a square circle. The forbidden shape simply does not exist.

riba_disguised.fiqh — refused

$ deducible check specs/riba_disguised.fiqh
✗ RIBA-1   capital_guarantee returns capital whole regardless of outcome — riba.
           al-Baqarah 2:275 · AAOIFI SS No. 12
✗ RISK-1   loss does not follow ownership; a partner who cannot lose is not a partner.
✗ GHARAR-1 valuation source is unspecified (majhul).
   no contract emitted.

How it is built

deducible is a pure-Rust compiler with a familiar pipeline:

lexer → parser → AST → sema (the fiqh invariant engine) → codegen
                                                          ├── Solidity + Hardhat test
                                                          └── portable invariant manifest (JSON)

The rule-base is data, not code: per-authority modules (e.g. AAOIFI, DSN-MUI) declare the invariants a contract must satisfy and the citation behind each. The engine is regime-neutral — it also models common-law commercial contracts — so the same machine can check gharar in one jurisdiction and penalty-clause doctrine in another.

What it does not do

A machine does not issue a fatwa. Deducible proves that a contract is consistent with rules a human scholar authored and cited — every time, identically, for anyone to verify. It does not decide what is halal. See The epistemic boundary.