Choose a contributor route

Choose by the first edit seam and smallest falsifying gate, not by a reading list. Routes labelled “role lab” have complete generated labs; remaining routes start at existing references.

Frontend / language

Change parsing, surface syntax, diagnostics, or type checking.

Start: role lab

First seams:

First bounded change: Add or adjust one checked syntax or elaboration fixture.

Narrow gate:

nix develop --command just check Bang/Frontend/TypeCheck.lean

Full gate:

nix develop --command just verify

Kernel / proof

Work on graded-CBPV semantics, typing, soundness, or a bounded proof obligation.

Start: role lab

First seams:

First bounded change: Close or adapt one small lemma without changing a frozen headline statement.

Narrow gate:

nix develop --command bash -lc 'just check Bang/Core/Soundness.lean && just axioms'

Full gate:

nix develop --command just verify

Machine / backend

Trace source meaning through CalcVM, compilation, execution, or Wasm emission.

Start: role lab

First seams:

First bounded change: Trace one constructor through source, compile/exec, and its differential fixture.

Narrow gate:

nix develop --command just check Bang/Backend/AbstractMachine.lean

Full gate:

nix develop --command just verify

Tooling / docs / examples

Improve generated facts, checked examples, diagnostics, or contributor tooling.

Start: role lab

First seams:

First bounded change: Add one generated fact, checked example, or diagnostic projection without copying its source fact.

Narrow gate:

nix develop --command bash -lc 'just check-examples && just check-examples-env && just docs-check'

Full gate:

nix develop --command just verify

Coding agent

Retrieve the authority, isolate the work, make one bounded edit, and report observed evidence.

Start: existing reference

First seams:

First bounded change: Identify the source of truth and complete one issue-sized edit in an isolated lane.

Narrow gate:

just fitness

Full gate:

just verify