tauto

A Language and Toolchain for Business-Rule Contracts

A Lean-backed system for authoring, validating, and testing business logic
Rust core · Lean 4 proof workspace · web interface

1 Introduction

Business rules—a prime mortgage may be approved only if the credit score is at least 750 and employment is verified—are typically scattered across code, documentation, and institutional memory. When a new rule is proposed, no one can easily answer the two questions that matter most: is it consistent with the rules we already have? and what tests would establish that an implementation obeys it?

tauto addresses both. Rules are written once, in a small language readable by domain experts and machines alike, and stored as ordinary Markdown. The toolchain then treats the rule set as a formal object: it detects pairs of rules that cannot both hold, generates conformance tests, and produces a Lean 4 scaffold for eventual mechanized proof. The design goal is the lowest possible barrier to entry: an author needs only a text editor, and a consumer—human or automated agent—needs only a single HTTP request to check a proposed rule.

2 The Contract Language

A contract is introduced by a fenced code block tagged contract. It consists of a case name and a sequence of labelled sections.

2.1 Grammar

A condition compares a field path against a typed literal:

The three literal kinds are distinguished lexically: 750 is an integer, true / false are booleans, and an identifier beginning with an uppercase letter (e.g. UnderReview) is an enum member. Field paths (loan.credit_score) refer to attributes of the entity or of the operation's result.

2.2 Section semantics

2.3 A worked example

```contract
case ApprovePrimeMortgage
entity:
  Mortgage
operation:
  approveApplication
requires:
  loan.credit_score >= 750
  loan.debt_to_income_ratio <= 40
  loan.employment_verified == true
  loan.income >= 60000
  loan.status == UnderReview
ensures:
  result.status == Approved
  result.interest_rate == Standard
  result.max_term_years == 30
forbidden:
  disburseFunds(loan.id)
preserves:
  loan.applicant_id
  loan.property_address
assumes:
  loan.credit_score > 0
```

This reads: to approve a prime mortgage application, require a credit score of at least 750, a debt-to-income ratio no greater than 40, verified employment, income of at least $60,000, and a status of UnderReview; the result must be an Approved loan at the standard rate for a 30-year term; funds must not be disbursed within the approval step; and the applicant's identity and property address must be preserved.

3 Consistency and Conflict Detection

Two rules governing the same (entity, operation) pair are in tension when they guarantee incompatible outcomes. tauto groups contracts by their operation key and inspects the ensures sets for contradictions.

When a candidate is found, tauto reports the two case keys and a human-readable reason, e.g.

Mortgage/approveApplication/ApprovePrimeMortgage
  ↔ Mortgage/approveApplication/LegacyRejectPrimeApplication
  reason: `result.status` cannot be both `Approved` and `Rejected`

Crucially, a contradiction in ensures is a conflict only when the two rules can actually apply to the same input — when their requires sets can hold simultaneously. Two rules guarding disjoint states (ship of a Paid order → Shipped vs an Unpaid order → Rejected) are distinct transitions of the entity's lifecycle, not a contradiction. tauto therefore suppresses a candidate whose preconditions are mutually exclusive — a shared field with disjoint constraints, e.g. == Paid vs == Unpaid, or ≥ 750 vs < 750.

4 Test-Suite Generation

For each contract, tauto emits a structured (JSON) test suite with two families of cases.

1. Happy path. One case in which every precondition is satisfied; the expected result asserts each ensures postcondition, that no forbidden operation is called, and that every preserves field is unchanged.
2. Precondition violations. For each condition c ∈ R, one case that satisfies every precondition except c; the operation must be rejected.

Boundary values are chosen to probe the exact edge of each comparison:

5 The Domain Glossary

Rules draw on a shared vocabulary: Mortgage has a credit_score; a Package has a weight_kg. Left implicit, this vocabulary drifts — the same concept acquires two field names, or a rule for one entity silently reaches into another's terms. The glossary makes the vocabulary explicit and checkable.

State fields tie the glossary to conflict detection (§3): a rule on a stateful entity should guard on its state field explicitly, naming the source state a transition starts from — a rule that does not is flagged missing_state_guard. Making source states explicit is what lets the detector recognise disjoint-guard rules as distinct lifecycle transitions rather than conflicts.

Given a glossary, tauto validates each contract's references and emits advisory warnings — it never blocks. For a field path p.f in a contract on entity E: if p is result or an alias of E, then f must be a declared field of E; if p is an alias of a different entity E′, the reference is flagged as cross-entity (the Order-vs-Package distinction); enum comparisons must use declared members. An empty glossary yields no warnings, so the mechanism is inert until a vocabulary is declared.

5.1 Lifecycle coverage

Because a state field carries its complete set of possible values, the rules can be read as a state machine: each rule is a transition from the state it guards on (in requires) to the state it produces (in ensures result.…). tauto assembles this graph per entity state field and reports coverage gaps — declared states with no incoming transition (a candidate initial or unreachable state), no outgoing transition (a candidate terminal or dead-end), isolated states touched by no rule at all (a likely gap), and any undeclared state a rule uses but the glossary omits.

5.2 State completeness from data

A glossary is declared first, before any data need exist — logic can be authored up front. When real datasets are present, their state domains can complete the declared ones. tauto reconciles the two: a state source yields the states observed for each field, and tauto reports, per state field, observed_not_declared (states in the data the glossary is missing — suggested completions) and declared_not_observed (declared but unseen — a future state or a typo). Source precedence is database → ODCS → file → none, reported in the response. The ODCS source reads any *.odcs.yaml (Open Data Contract Standard) contract in the contracts directory, taking a column's allowed values from its invalidValues data-quality rule (arguments.validValues) and mapping the schema object and property onto a glossary entity and state field.

The live-database state source (behind the database build feature, configured with DATABASE_URL) reads the distinct values of each state field's column — mapping entity Mortgage to table mortgage and a state field status to column status. Identifiers are validated against [A-Za-z_][A-Za-z0-9_]* and quoted before interpolation, so no schema-derived name can escape the query; an absent table or column is skipped, and an unreachable database falls back to the file descriptor.

6 The Lean Backend

tauto translates each contract into a Lean 4 theorem whose statement encodes “preconditions imply postconditions,” and assembles them into a lake project. Running lake build confirms that the generated statements are well-typed.

Compilation runs in a separate, pluggable build service rather than the web process, so the Lean toolchain never bloats the served image. The server POSTs the workspace to TAUTO_LAKE_URL under a minimal contract (POST {files:[{path,content}]} → {success,stdout,stderr}) that any Lake deployment can implement; tauto lake-worker is the reference implementation. When no builder is configured, the Proofs view degrades gracefully—it still generates and shows the obligations, only skipping the compile.

7 Using tauto

7.1 Quickstart

Write rules in a Markdown file, then serve the workspace:

# put contracts in ./rules/*.md, then:
tauto serve ./rules --port 4000
# open http://localhost:4000

7.2 Command-line interface

All commands accept --format json for machine consumption.

7.3 HTTP API

The server exposes a small JSON API under /api/v1. The endpoint of most interest to an automated agent is POST /check, which validates a proposed rule against the current set without persisting anything and returns both a compatibility verdict and a generated test suite.

# body is Markdown containing one or more contract blocks
curl -X POST http://localhost:4000/api/v1/check \
  -H 'Content-Type: text/plain' \
  --data-binary @proposed-rule.md

{
  "compatible": true,
  "proposed_contracts": 1,
  "parse_errors": 0,
  "conflicts": [],
  "tests": {
    "total_cases": 11,
    "proposed":   [ /* suites for the new rule */ ],
    "regression": [ /* suites for existing rules */ ]
  }
}

When the proposal contradicts an existing rule, compatible is false and conflicts lists each offending pair with a reason (Definition 3.1). An agent can thus gate a proposed rule on a single request and receive, in the same response, the tests an implementation must satisfy.

7.4 Web interface

tauto serve also hosts a browser UI: a force-directed graph of contracts (with conflict edges highlighted), a searchable list, an upload history, a proofs panel that runs lake build, and a check panel that mirrors POST /check—paste a rule, see the verdict and the generated test cases.

8 Limitations