Introducing a new scientific domain

Computational Halacha

Formal symbolic reasoning for Jewish law — encoding centuries of halachic logic into a verifiable, queryable knowledge system

Open the IDE Read the Paper

Mistaber — formal symbolic reasoning for Jewish law

What is Mistaber

Mistaber (מסתבר — "it stands to reason") is the first formal system that applies Kripke modal semantics and Answer Set Programming to encode the Shulchan Aruch as a computable knowledge base. Every ruling traces from code back to Torah through a verified source chain. Disputes between authorities are modeled as parallel worlds, not contradictions. The result: halachic reasoning you can query, compare, and formally verify.

Mistaber is a research tool for analyzing the formal structure of halachic reasoning — not a replacement for a human posek.

Core Foundations

Eight scientific contributions in one system

Kripke World Hierarchy

Seven halachic authorities modeled as possible worlds in a 3-tier DAG. Mechaber, Rema, GRA, and their modern successors — each with inheritance and selective overrides.

Answer Set Programming

Non-monotonic reasoning with Clingo. Rules with exceptions, negation-as-failure, and stable model computation — matching how halacha actually reasons about defaults and overrides.

Halachic Logic Language

A domain-specific language for encoding rulings. HLL compiles to ASP with mandatory source citations, madrega levels, and world scoping built into the syntax.

Agentic Encoding Pipeline

AI-assisted encoding with human-in-the-loop supervision. A 5-phase workflow with mandatory checkpoints — Claude Code fetches sources from Sefaria, encodes rules, and validates while humans approve.

Formal Ontology

69 predicates, 29 sorts, disjointness constraints. Covers foods, vessels, mixtures, actions, normative statuses, safek calculus, and provenance chains across domains.

Derivation & Explainability

Every ruling comes with a complete proof tree. Trace any conclusion through its derivation back to Torah — full provenance and source chain for every answer the engine gives.

See it in action

Compare rulings across authorities

  query.py 
# Is fish with dairy forbidden?
# Compare across authorities

from mistaber.engine import HsrsEngine

engine = HsrsEngine("mistaber/ontology")

result = engine.compare(
    "holds(issur(achiila, M, L), W)",
    worlds=["mechaber", "rema"]
)
mechaber
holds(issur(achiila, dag_chalav, sakana), mechaber)
makor: Shulchan Aruch YD 87:3
issur · sakana
machloket detected — fish & dairy
rema
holds(mutar(achiila, dag_chalav), rema)
makor: Rema gloss on YD 87:3
mutar · no sakana

The Workbench

A browser-based IDE for encoding halacha

The Mistaber IDE provides a complete environment for encoding, validating, and reviewing halachic rules — with an integrated Claude Code terminal for AI-assisted workflows.

  • Session & phase management
  • Interactive ontology browser
  • ASP query executor
  • Integrated terminal
  • Derivation tree viewer
  • Coverage dashboard
  • Monaco code editor
  • Validation reports
Open ide.mistaber.ai
$ mistaber compare "holds(issur(A,M,L),W)" \
    --worlds mechaber rema ashk_mb
 
Comparing across 3 worlds...
 
mechaber — issur(achiila, dag_chalav, sakana)
rema — mutar(achiila, dag_chalav)
ashk_mb — mutar(achiila, dag_chalav)
 
Machloket detected: fish & dairy
mechaber vs rema on sakana(dag_bechalav)
 
$ mistaber explain "holds(issur(...), mechaber)"
Derivation tree (depth 4):
SA YD 87:3 → sakana(dag,chalav) → issur(achiila)
Verified: chain reaches Torah source