Are you an LLM? Read llms.txt for a summary of the docs, or llms-full.txt for the full context.
Skip to content

Development

Layout

DoreFormal/        the Lean 4 development — 81 targets, no sorry, no axioms
dore-contracts/    Hardhat project — 4 contracts, 19 tests
docs-site/         this documentation
encyclopedia/      the product corpus and the legal source registry

The formal development

lake build          # 81 targets
.claude/bin/loop-test   # build + hygiene gate

The hygiene gate fails on any sorry, admit, native_decide, custom axiom or compiler warning. Axiom audits are run on every headline theorem; the development uses only propext, Classical.choice and Quot.sound, and many results use none.

The contracts

cd dore-contracts
yarn install
npx hardhat test

Tests are named after the theorems they discharge. If a contract changes such that a named property no longer holds, the test that fails tells you which proof you have contradicted.

The documentation

cd docs-site
npm install
npm run dev        # local
npm run build      # static output in dist/

House rules

Never claim a theorem that does not exist. A docstring in this project once named a theorem as the thing binding two halves of a module together; the theorem did not exist, and the halves were unconnected. Grep every name you cite before shipping.

Report frontiers, not tuned successes. Where a result depends on an unverified input, publish the boundary at which it changes rather than picking an input that makes it pass.

Say what is not modeled. Each module carries an explicit "is not grounded" section. Those sections are the most useful part of the development to a reader deciding how much weight to put on it.