14 October 2026

Rifat Jumagulov · How this is checked

What If Knowledge Itself Could Be a Software Dependency?

Public repositories show what modelling on Arxo looks like: constitutions, civil codes, a tax code, treaties, benefit and insurance rules, the Laws of Chess, physics, chemistry, biology and philosophy, all on one language and runtime. They are a small sample of a much larger corpus of models.

In Arxo's OpenStax friction example, an applied force of 80 N against a maximum static friction of 80 N returns TRUE_ONLY for "stays at rest". Change the applied force to 90 N and it returns FALSE_ONLY. The rules and their premises are recorded in a proof graph.

The same runtime answers questions about a French debt, a Japanese parliamentary vote, a US earned income credit, a chess arbiter's ruling, a first-order reaction, a monohybrid cross and Aquinas's account of self-defence.

Each model is a versioned dependency: named, pinned to its sources, and reusable by applications. Install the runtime, load a model, supply facts and a date, and inspect the result.

Arxo is executable knowledge infrastructure. The reusable artifact is an explicit interpretation of a source, packaged with its rules, dependencies and examples. A language model can help author it; Arxo executes it.

Run one

The CLI examples use Node.js 20 or newer on macOS arm64 or Linux x64. Install the pinned runtime, then follow the selected repository's example commands. For mechanics:

npm install -g @arxo/cli@0.2.4
git clone https://github.com/arxohq/arxo-openstax-mechanics.git
cd arxo-openstax-mechanics
law eval examples/friction-at-limit
law eval examples/friction-above-limit

The first example supplies an applied force of 80 N, a normal force of 200 N and a static coefficient of 0.4. The model derives the maximum static friction, 0.4 × 200 N = 80 N, from the rule of section 6.2 of the textbook, compares with units, and answers COMPUTED / TRUE_ONLY. The second raises the force to 90 N: COMPUTED / FALSE_ONLY. The repository contains no second implementation of the formula; the model does the arithmetic.

Why "dependency" is the right word

A dependency has a name, a version, a lock file and imports. openstax.dynamics@0.1.0 imports openstax.kinematics, openstax.measurement, units.si, bipm.si_brochure and, as its historical axiomatic layer, la.newton.principia. A lock pins the closure, so the friction answer reproduces without fetching anything. Five models cover selected chapters of University Physics Volume 1, from measurement to rotation, with twelve runnable examples.

The Code civil repository separates limitation, contract, liability and succession into versioned packages and includes a historical 1804 model. A case package that needs them declares them, like any manifest, and the answer document records the manifest of package versions it evaluated.

Versioning is also what makes editions tractable. The mechanics repository includes the same collision facts evaluated against two pinned OpenStax source editions, before and after a published correction: NEITHER in the earlier edition, TRUE_ONLY in the later one. The example selects the source edition through its temporal context, not through a branch of code.

Public demonstrations: a sample of the corpus

The public repositories are demonstrations. They are a small sample of a much larger corpus of models on Arxo, chosen to show what modelling looks like across subjects. Each one states its scope per package, pins its sources and records its cases with their answers.

Two companion repositories hold the fictional case packages of the Law as Code in Practice books for France and Germany. The catalogue of packages, repositories and tools is github.com/arxohq/law.

Four more bodies of knowledge

FIDE Laws of Chess. In the supplied SecondIllegal case, two completed illegal moves under the model's declared closure produce COMPUTED / TRUE_ONLY for the loss query: Article 7.5.5. The companion case establishes that the opponent cannot checkmate by any series of legal moves; the draw query returns COMPUTED / TRUE_ONLY, and the separate loss query returns REQUIRES_JUDGMENT, because other loss grounds in the Laws still call for an arbiter. The model library ships with a typed Node.js loader and ten retained arbiter cases; a separate MCP package runs the same pinned model.

Code civil. A claim became enforceable on 1 January 2000; proceedings began on 1 January 2015. The case supplies uninterrupted limitation, with no suspension in the modern reading. Is the claim time-barred? Applying the pinned 1804 model gives COMPUTED / FALSE_ONLY: its thirty-year period has not elapsed. Applying the modern limitation model, captured on 16 September 2026, gives COMPUTED / TRUE_ONLY. The 2008 transition starts the shorter period on 19 June 2008 and ends it at the close of 18 June 2013, following the calculation cited from the Cour de cassation. The examples apply two explicitly selected historical readings to the same debt facts. Selected fields from the saved prescription-actuelle answer:

{
  "resultKind": "PROPOSITION",
  "target": "urn:fr:corpus:clir:code-civil#action_prescrite_le",
  "evaluationStatus": "COMPUTED",
  "truthStatus": "TRUE_ONLY"
}

Constitution of Japan. In the example, eight votes out of all twelve members of one House satisfy Article 96's House-level initiation threshold: COMPUTED / TRUE_ONLY. Seven votes give COMPUTED / NEITHER. The model distinguishes thresholds based on members present, all members and votes cast, and handles tied votes separately, because the Constitution does.

Summa Theologiae. A traveller under attack intends to preserve life. The case explicitly states that death is neither intended nor used as a means, and supplies an adjudicated assessment of proportionate force. Under the selected respondeo of II–II q. 64 a. 7, defensio_licita returns COMPUTED / TRUE_ONLY. Remove the proportionality assessment and it returns REQUIRES_JUDGMENT / NEITHER, identifying the assessment and its declared authority. The model does not replace that judgment with a force threshold.

What a model is made of

Three excerpts from the public model sources, with selected explanatory labels omitted.

Chess, Article 7.5.5:

@source(FIDE_ART_7)
rule SecondIllegalMoveLoses(game: Game, who: Player, n: Integer) strict {
    label en official "Article 7.5.5. For the second completed illegal move by the same player the arbiter shall declare the game lost by this player";
    when player_of(game, who)
        and completed_illegal_move_count(who, n)
        and (n >= 2)
        and not king_cannot_be_checkmated(who);
    then game_lost_by(game, who);
}

Code civil, the 2008 transition:

@source(CC_POST_ART2222, CC_POST_ART2228, CC_POST_ART2229, REFORM_ART26)
rule EcheanceTransitoireCinqAns(c: Causa, premier: Date, veille: Date) strict {
    label fr official "le délai transitoire de cinq ans expire à la fin de la veille du même quantième";
    when delai_transitoire_court_des_le(c, premier)
        and reforme_2008_publiee_le(veille)
        and add_calendar_period(veille, 1 calendar_day) == premier
        and prescription_non_interrompue(c);
    then echeance_prescription_le(c, add_calendar_period(veille, 5 calendar_year));
}

Summa, I–II q. 90 a. 4:

@source(ST_Q90_A4_RESP)
definition is_law(l: Law) exact {
    label la official "quaedam rationis ordinatio ad bonum commune, ab eo qui curam communitatis habet, promulgata";
    when ordinance_of_reason(l)
        and ordered_to_common_good(l)
        and issued_by_caretaker_of_community(l)
        and promulgated(l);
}

The same handful of constructs carries all of it. Entities and relations are typed; a relation is either empirical, supplied by the case, or institutional, derived by the model. A rule is strict or defeasible, and defeasible rules carry priorities, so a special provision can defeat a general one without rewriting either. A definition marked exact makes its conditions jointly sufficient and each one necessary. Rules reference source fragments through @source; content hashes identify the exact source bytes used by the model, so a reviewer can follow each rule to that pinned text and examine the interpretation. Dates are first-class: a question is asked at a legal time, and the edition in force on that date answers it. Where the source hands a question to an authority, the model asks for an adjudicated fact instead of guessing.

The chess example declares where its mate-possibility facts are complete. Within that declared scope, a closure rule derives an explicit negative, and the loss rule uses it. Supplying the positive inability-to-mate fact establishes the draw. Outside an explicitly declared closure, absence alone supplies no negative fact.

What an answer is made of

An answer is not a boolean. For a proposition query, truth status and evaluation status answer different questions. TRUE_ONLY, FALSE_ONLY, BOTH and NEITHER distinguish positive support, negative support, conflicting support and support for neither side. REQUIRES_JUDGMENT identifies an unresolved assessment and its declared authority. An established conclusion can coexist with a pending judgment. NEITHER records that the selected model and supplied facts establish neither the proposition nor its negation.

The answer document records applied rules and their premises in a proof graph, together with judgment requests and canonical hashes. In the chess SDK, answer.proof.nodes identifies the executed rules; the README shows how to join those identifiers to source anchors in the pinned model. With the same pinned model, runtime and complete explicit input, repeated execution reproduces the canonical answer bytes.

From authoring to execution

Formalization happens before execution. A language model can draft a model under compiler diagnostics; reviewers can inspect its rules against the pinned source. Arxo then evaluates the versioned model over explicit case facts, and the answer is the same every time. Where the source leaves a judgment to a court, an arbiter or a reader, the answer says so and names the authority.

The neighbours, and a question

Logic programming, proof assistants and computable knowledge systems are the relevant neighbours: Prolog and Datalog, Lean, Wolfram and Cyc. Arxo's delivery unit is a versioned interpretation of a source, carrying typed rules, applicability conditions, source editions, dependencies and inspectable derivations. Applications consume that package through a common execution interface.

Take one example from any of the repositories, change a fact and inspect the derivation. Which source would you package next, and what would its consumers need to reproduce an answer after the source changes?

• Start with any repository in the table above. The catalogue, SDK and CLI live at github.com/arxohq/law.