Skip to content

In the open

Deducible is open source under the MIT license, at github.com/dihannahdi/deducible. The repository is the whole compiler: the Rust crates, the rule modules, the spec corpus, the generated-contract toolchain, and the papers. Nothing about the engine is hidden. That is the point. A compliance claim you cannot inspect is just another promise.

The compiler is pure Rust. The CLI binary is deduce.

Terminal window
git clone https://github.com/dihannahdi/deducible
cd deducible/fiqh-compiler
cargo test # the engine + every per-instrument suite
cargo run --bin deduce -- --help
deduce check specs/riba_disguised.fiqh # MUST be refused (exit 1, no .sol)
deduce build specs/murabahah.fiqh --root . # emit a murabaha contract + test + manifest
deduce check specs/musharakah_mutanaqisah.fiqh --rules maliki # refused (profit_tracks_capital)
deduce check specs/musharakah_mutanaqisah.fiqh --rules hanafi # consistent (the khilāf)

The repository layout:

crates/fiqhc/src/ lexer, parser, ast, sema (the invariant engine), codegen, maqasid, zakat,
faraid, composite, zk, lsp, nl
specs/ one positive and one negative-control .fiqh per instrument
rules/ aaoifi, dsn-mui, hanafi, maliki, shafii, hanbali (pluggable rule modules)
paper/ the four design-science papers

A note on naming. The project and brand are Deducible. The CLI command is deduce (you deduce a contract’s compliance). The Rust library crate is internally fiqhc, a code-level legacy detail; you will see it in paths and FFI symbols.

This is the contribution that scales. A rule module is plain JSON: per class, the required invariants and the { code, field, op, value, citation } constraints that encode an authority’s position. Authoring one needs fiqh and citations, not Rust.

  • Encode a well-sourced madhhab khilāf the current modules do not yet carry. All six modules now have an entry for all 26 classes in the catalogue, so this is no longer “extend coverage” but “find the next real divergence”: two are encoded so far (musharakah mutanaqisah’s profit_tracks_capital, rahn’s amāna/ḍamān split); Rule modules names several considered and declined for lack of a firm-enough citation; a scholar closing one of those is exactly the contribution that scales.
  • Firm up an “honest gap” citation. A handful of classes carry classical-basis citations because no dedicated AAOIFI Standard or DSN-MUI fatwa exists (see the same reference page); a contributor who can supply the primary Himpunan Fatwa reference for a DSN-MUI number currently missing its Roman-numeral month code closes a real, named gap.
  • Encode another body’s standard (a national fatwa council, a bank’s own Shariʿah board) as a new rules/<name>.rules.json.
  • Every constraint must carry a citation. Modules ship [scholar-verify] and must be ratified by a qualified authority before any reliance. The engine ratifies nothing.

See Rule modules for the schema, the coverage table, the live khilāf examples, and the checker-grammar gaps (lt/le, cross-field equality, OR-of-values, the pool.* path) that block a few further constraints today: good first engine issues for a contributor who would rather touch sema.rs than fiqh citations.

Adding a class touches a known set of files: a variant and check function in sema.rs, a generator in codegen.rs, a positive spec and a negative control in specs/, and a test. The catalogue shows the pattern the existing classes follow. Good candidates are the variants the catalogue notes as folded rather than separate, and the structural gaps (livestock per-head zakat, for one).

The specs/ corpus pairs each instrument with a negative control that must be refused, so every addition both demonstrates the licit form and pins the forbidden one. The fuzz harness (deduce fuzz) runs the front-end and engine over random and mutated input inside catch_unwind; it should never panic. The LSP, the C-ABI/Wasm FFI, and the invariant gateway are all open for editor integrations and embedding. See Integration & APIs.

The paper/ directory holds four design-science papers tracing the work from one instrument to the breadth of muʿāmalāt:

  1. The compliance-by-construction instrument and its live artifact.
  2. Algorithmic jurisprudence: the compiler and its expansion visions.
  3. Beyond the bilateral contract: the doctrines that surround the ʿaqd (the five C’s).
  4. The whole economy: the extension from four instruments to the full catalogue, the pool primitive, and the madhhab modules.

Read this before relying on anything here. Deducible proves a spec is consistent with a human-authored, citation-bearing rule-base. It issues no fatwa, and a testnet deployment proves execution, not legitimacy. The rule modules and citations require ratification by a qualified scholar before any reliance. See The epistemic boundary. Allāhu aʿlam.