Gentzen — Auditable Rule-Based Reasoning for Agent Decision Gates

An engine for agents to determine what is the case in the world before acting, and to produce a step-by-step proof of that determination that survives compliance audit and post-hoc review.

What this is

Agents take real actions. Before each action, you need an answer to: given the current state of the world, which of these actions are justified?

Gentzen answers that as a per-target verdict table. You write business rules once, in YAML, as compound propositions like ((CustomerVerified ∧ NotFlagged) → ProcessOrder). Resolver functions observe the world — databases, APIs, clocks, queues. The engine then reports, for every candidate action you declare, one of three outcomes.

switch (target.outcome) {
    case 'proven':     /* the rules and the observed world derive this */
    case 'refuted':    /* the search completed; this does not follow   */
    case 'incomplete': /* nothing was decided — do not call this a no  */
}

The distinction between the last two is the point of this library. "I proved this action is not justified" and "I ran out of road" are different claims about the world, and only the first belongs in an audit log as a refusal. When the outcome is 'incomplete', incompleteReason says which bound was hit, and missingFacts names the sensors that never reported.

A second distinction sits inside 'proven'. The derivation field says how: 'inference' and 'derived' mean the engine worked it out; 'fact' means a resolver said so directly; 'asserted' means the scenario declared it and the engine did no work at all. Gate on outcome === 'proven' && derivation !== 'asserted' — never on a boolean alone.

Two further guarantees:

• Resolver failures abort the run. A throw or rejection is a sensor outage, not a false answer. The scenario returns { aborted: true, reason: 'resolver_error', resolverName, cause } and the agent must not act. Relatedly, only boolean true asserts a fact — a resolver that returns a payload, an Error, or nothing at all fails closed.
• Every derived result carries an auditable chain — a structured list of which rules fired on which premises. Pipe it into your audit log; render it for humans.
• Resolvers can record what they saw, not only what they concluded. observe({ amount, threshold, currency }) files evidence against an atom and attaches it to the matching leaves of the proof. The evidence is inert — the engine never reads it — so a chain gains its content without any change to the reasoning.

Where this sits

Gentzen is a deterministic gate for the moment an agent is about to do something irreversible. The usual tools for that job are a wall of if-statements (no audit trail, no unknown-tracking, a closed world), a JSON-rules engine (boolean evaluation, no proof, no missing-sensor diagnosis), a policy platform like OPA/Rego (heavyweight, its own language, closed-world defaults), or letting the model decide (no guarantees at all). Against all four, the claim here is narrow and checkable: the engine proves an action follows, proves it does not, or names exactly what is missing — with a derivation chain that re-derives independently, evidence attached to its leaves, and refusals backed by a completed fixpoint rather than an exhausted budget.

Agents are taking real actions on real systems, and the layer between the model wants to and the system does has to be deterministic, auditable, and honest about what it does not know. That layer is what this library is. Its claims are measured, not asserted: yarn verify re-proves soundness exhaustively against an independent oracle, re-measures the scale envelope, and fails on any regression — see verification/.

What this is not

Not a general-purpose theorem prover. The engine implements a focused fragment of classical propositional logic suited to decision-gating: modus ponens, modus tollens, contraposition, double negation, conjunction introduction and elimination, disjunction introduction (both the classical one-premise form and a both-premises form), disjunction elimination, disjunctive syllogism, and disjunctive modus ponens.

It does not introduce implications or biconditionals from arbitrary pairs of formulas — those require discharging an assumption, and omitting them is what keeps the search simple and terminating. Declare them as propositions instead. See docs/logical-rules.md.

New to formal logic?

You do not need a logic background to use this, and you should not have to acquire one to trust it.

• Core Ideas in Plain Language — twenty minutes, no symbols. What a proposition is, what "provable" means, why asserting is not deriving, and why failing to prove something is not the same as disproving it.
• Gentzen Logic 101 — a complete sixteen-chapter course with a workbook and worked solutions, from "what is an argument" to how a .yaml file becomes a proof tree. Assumes nothing.

Quick start

git clone https://github.com/bulldogandfisk/gentzen.git
cd gentzen
yarn install
node examples/demo-agent-gate.js

import { join } from 'node:path';
import { runGentzenReasoning, isAbortedResults } from 'gentzen';

const results = await runGentzenReasoning(
    join(import.meta.dirname, './scenarios/mixed-scenario.yaml'),
    { resolversPath: join(import.meta.dirname, './resolvers') }
);

if (isAbortedResults(results)) {
    // A sensor is down. There is no verdict table. Do not act.
    console.error(`Aborted: ${results.resolverName} — ${results.cause}`);
    process.exit(1);
}

for (const target of results.targets) {
    if (target.outcome === 'proven' && target.derivation !== 'asserted') {
        console.log(`OK to ${target.formula}`);
    } else if (target.outcome === 'refuted') {
        console.log(`Refused ${target.formula} — does not follow`);
    } else if (target.outcome === 'incomplete') {
        console.log(`Undecided ${target.formula} — ${target.incompleteReason}`,
                    target.missingFacts);
    } else {
        console.warn(`Refusing to gate on ${target.formula} (asserted only)`);
    }
}

examples/demo-agent-gate.js runs this same scenario three times — all sensors true, one sensor false, and one sensor absent — so you can see proven, refuted, and incomplete produce three different agent behaviours on the same rule.

Documentation

Full documentation lives in docs/.

| Document | Description | |----------|-------------| | Core Ideas | The concepts, in plain language, with no prerequisites | | Gentzen Logic 101 | Sixteen-chapter course in propositional logic, plus workbook | | Getting Started | Install, first scenario, first verdict | | Scenario Guide | Writing YAML scenarios: rules as propositions, resolvers as sensors | | Scenario Author Checklist | Prescriptive dos and don'ts; pre-deployment review checklist | | Logical Rules | Every inference rule with formal definition and business example | | Operator Reference | Operators, aliases, precedence, formula syntax | | Resolvers | Writing, organising, and debugging resolver functions | | Architecture | System internals — modules, data structures, configuration | | Proof Engine | The search algorithm and derivation-path building | | API Reference | Complete API surface — exports, options, config keys, return types | | Integration Patterns | Agent gates, batch processing, what to do with each outcome | | Performance | Cost model, tuning knobs, benchmark baselines | | Troubleshooting | Symptom-to-cause guide |

Testing

yarn test               # Unit + integration + coverage gate, then all examples
yarn test:unit          # Unit tests only
yarn test:integration   # Integration tests only
yarn test:performance   # Performance suite (excluded from the default run)
yarn test:examples      # Run all 14 examples
yarn bench              # Proof-search benchmark
yarn verify             # Verification harness: soundness, envelope, mutation, baseline
yarn verify:nightly     # Widest profile; writes a dated report and trend history

Requirements

Node.js ≥ 24.

License

SSPL-1.0