colregs-engine

Two vessels are closing. What must they do? Who gives way? What must they display?

The COLREGS, the International Regulations for Preventing Collisions at Sea, answer all three. This project transforms the colregs so that a machine can evaluate and reason about them deterministically: the whole of the rules as structured data, so the same situation always yields the same result, and every result can be traced back to the rule that produced it. Going further, the engine and the rules are then checked with formal methods, which means mathematically proving the rule set is consistent and complete rather than just testing it a bunch and hoping it all works out.

Related packages:

• colregs - the data and JSON Schema
• colregs-engine - the engine that evaluates rules
• colregs-mcp - an MCP server so AI can use the engine
• nav-wright - draws vessels and displays (stub)
• searoom - a study tool demo

See a live demo of searoom and the colregs data/engine.

Usage

One call. Pass a fact record describing one vessel at one moment and get back every complete lawful display.

import { evaluateSignals } from 'colregs-engine';

const result = evaluateSignals({
  'fact:propulsion': 'propulsion:sail',
  'fact:activity': 'activity:none',
  'fact:position': 'position:underway',
  'fact:length_m': 11.6,
});

For that 12 m sloop the result is three displays, because Rule 25 offers a choice and the engine never picks for you:

applied:  25a, 25b, 25c
displays:
  chosen [25b]   combined lantern[may]
  chosen []      sidelights[shall], sternlight[shall]
  chosen [25c]   sidelights[shall], sternlight[shall], all-round red[may], all-round green[may]

The order is the order to consider the rules in: the most specific concession the Convention wrote for this vessel first (25(b) below 20 m), the rule as written last. Take index 0 for the usual display.

Every light in a display names the entry that prescribes it (source_entry), the entry that pulled it in if different (via), and how strongly the rule requires it (modality). Every display names the choices that produced it (chosen), so a UI can let the user eliminate options.

When one rule vetoes another, the result says who did it. A fishing vessel aground:

evaluateSignals({
  'fact:propulsion': 'propulsion:power',
  'fact:activity': 'activity:fishing',
  'fact:position': 'position:aground',
  'fact:length_m': 30,
});

applied:  26c-id, 30d-anchor, 30d-red
excluded: [{ id: "30a", by: "26c-id" }, { id: "30b", by: "26c-id" }]
displays:
  chosen []   all-round[shall], all-round[shall], all-round[shall-if-practicable]

Rule 26(a) says a fishing vessel shows only the lights in that Rule, so the ordinary anchor lights are struck and reported as excluded. The aground signal of Rule 30(d) still stands.

Fact keys and values are the identifiers in colregs' data/facts.json, and the types are generated from it: { propulsion: 'sail' } does not compile, because the key is not namespaced and the value is not one Rule 3(c) knows. Both are also checked at runtime, so a record that arrives as JSON or through a cast is rejected too:

import type { FactRecord } from 'colregs-engine';

evaluateSignals({ propulsion: 'sail' } as unknown as FactRecord);
// Error: unknown fact key 'propulsion'; did you mean 'fact:propulsion'? …

A malformed record is an error, not an empty display; an empty display is the honest answer for a vessel that lawfully shows nothing, and the two must not look alike. The envelope's applied is just the matching entry ids, in data order: the fixture contract, and the only list of them.

evaluateCircumstances(situation) reads two vessels at one instant: encounter type, each vessel's roles, what overrode what; every case of colregs' situation-fixtures.json replays. evaluateCompliance(trace) and evaluateDeparture(situation, model) are partial: the window and the Rule 13(d)/17 phases with every verdict pending, and a region lookup in the model's regions, else inconclusive-in-model. The envelope says what it could not decide: nothing throws for want of data, though a malformed situation, trace or model still does. The shapes and the opts.data / colregs.source contract are settled in colregs ADR 0011 and ADR 0012; the surface as a whole, one operation per thing and no companions, is proposed in colregs 0023, not yet ruled.

Entry points

From colregs-engine (src/index.ts). These are the engine's own vocabulary and do not move when colregs releases data.

Export	What you get
evaluateSignals(facts, opts?)	every complete lawful display for one vessel, plus which entries applied and which were excluded and by whom
DisplayEvaluation	the result: applied, excluded, displays, the per-entry categories, the provenance block and the colregs version stamp
EvaluationProvenance, RuleCategory, RepresentedParagraph, KnownOmission	what the evaluation read: categories, jurisdictions, Rule 2(a)/2(b) as represented but never computed, and known omissions
DepartureStatus	the closed status alphabet colregs' ADR 0005 §5 fixes, for evaluateDeparture; no field of DisplayEvaluation carries one
Display, DisplayLight, DisplayShape	one lawful display and one light or day shape in it, each citing source_entry, via and modality
FactRecord	the input, generated from colregs' facts.json
Modality	how strongly a light is required: shall, may, shall-if-practicable and the rest, as colregs defines them
evaluateCircumstances(situation, opts?), evaluateCompliance(trace, opts?), evaluateDeparture(situation, model, opts?)	scope, encounter type, risk grounds, roles and overrides for two vessels; the trace and departure verbs, partial as above
evaluate(circumstances, opts?)	the unified form, a second variant beside the three: one evaluation, its appraisal, signals and indicated read lazily

colregs-engine/schema (src/schema.ts) is the colregs data shapes generated from that package's JSON Schema: Entry, Predicate, LightSpec, ApplicabilityData and the rest. Import these only if you read the data files yourself; they change when the data changes.

Constraints

These exist so the engine can be checked exhaustively instead of sampled, which is what the next section is about.

• Pure and total. Facts in, displays out. No I/O, no clock, no state. Timing, freshness and hysteresis belong to whatever calls this.
• Finite input. Partition the numeric facts at the thresholds the rules actually compare against (7, 12, 20, 50 and 100 m, plus the tow, gear and speed constants) and the whole fact space is around 5 × 10⁶ records. Minutes of CPU.
• Complete answers. Where several displays are lawful, all of them come back. The fact record describes a situation, not a fitted vessel: nothing in it says whether a sloop carries a tricolour lantern, so nothing in it could settle Rule 25(b) against 25(c). Narrowing the set would take a fact the engine is not given. Composition itself is a different matter — the engine makes the judgment calls the data leaves open, each recorded in docs/engine-notes.md.
• Traceable. Every entry in an output cites the paragraph it came from.

Verification

"Does the engine agree with the rules?" should be answered by checking every case, or by proving it. Each step below is a stronger answer than the one before.

0. Fixture replay: the package's fixtures/applicability-fixtures.json, verbatim. The least it should pass.
1. Exhaustive conformance, in CI. npm run conformance walks all 11,860,992 records of the partitioned fact space and checks that engine output equals the set of entries whose conditions hold, against a second reading of the predicate semantics written independently of src/. The same run looks for conflicting shall entries, records that end up with no obligation at all, entries and branches that never fire, and cites that don't resolve to a paragraph. Whatever it finds is printed as a readable vessel and saved as a fixture in research/conformance/, which explains how to run it and how a finding is triaged.
2. The same properties handed to a solver: Z3 over the applicability table (research/z3/), Alloy for the encounter sectors. This is for anyone who distrusts "we ran a lot of tests", which is a reasonable thing to distrust.
3. A Rocq proof that partitioning at the thresholds misses nothing, which promotes step 1 from a big test to an actual proof.
4. Maybe a verified evaluator: the core written in Gallina, proved total and deterministic, extracted, then run as a second implementation against step 1's harness. Worth deciding once step 3 lands.

Steering rules are a separate problem — Part B, three-vessel cycles, timing and kinematics — and they're tracked with the rest of the programme in colregs-engine#1.

New to the tooling? There's a glossary and a reading list.

Licence

Apache-2.0. Nothing here is advice to mariners; the fitness-for-navigation disclaimer in colregs carries over.