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.
Clone, build, run
Section titled “Clone, build, run”The compiler is pure Rust. The CLI binary is deduce.
git clone https://github.com/dihannahdi/deduciblecd deducible/fiqh-compiler
cargo test # the engine + every per-instrument suitecargo 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 + manifestdeduce 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, nlspecs/ one positive and one negative-control .fiqh per instrumentrules/ aaoifi, dsn-mui, hanafi, maliki, shafii, hanbali (pluggable rule modules)paper/ the four design-science papersA 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.
Where contributions help most
Section titled “Where contributions help most”1. Rule modules (the first ask)
Section titled “1. Rule modules (the first ask)”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.
2. Instruments
Section titled “2. Instruments”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).
3. The corpus and the tooling
Section titled “3. The corpus and the tooling”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 papers
Section titled “The papers”The paper/ directory holds four design-science papers tracing the work from one instrument to the
breadth of muʿāmalāt:
- The compliance-by-construction instrument and its live artifact.
- Algorithmic jurisprudence: the compiler and its expansion visions.
- Beyond the bilateral contract: the doctrines that surround the ʿaqd (the five C’s).
- The whole economy: the extension from four instruments to the full catalogue, the pool primitive, and the madhhab modules.
The standing boundary
Section titled “The standing boundary”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.