15. Credo Plugin: Opt-In Linter for TLA+ Formality

Copy Markdown

Date: 2026-04-26

Status

Accepted

Context

ADR-0014 establishes a three-layer model for strictness decisions at the Elixir↔TLA+ boundary. Layer 3 — prescriptive linting — was deferred to a separate ADR because it is an implementation choice independent of the architectural pattern.

This ADR addresses Layer 3.

The need is concrete. Even with Layer 1 (permissive DSL) and Layer 2 (validating emitter) in place, a project publishing reference specs alongside ADRs has no automated way to enforce the conventions it cares about: that constants are declared explicitly, that DSL nesting doesn't trigger Spark's non-fatal FunctionClauseError warning. Without a linter, the conventions live in CONTRIBUTING.md and depend on reviewer vigilance. With one, they're enforced by mix credo in pre-push hooks.

The decisions in scope are:

  1. Packaging. Standalone tlx_credo package, or bundled with TLX?
  2. Discovery. Auto-loaded by Credo when TLX is a dep, or registered via .credo.exs?
  3. Default state. Checks enabled by default, or opt-in?
  4. Categorization. Use Credo's standard categories, or invent new ones?
  5. Initial check set. Which checks ship in the first cut?

Several alternatives were weighed for each. The salient ones:

  • Standalone package. Familiar pattern (e.g. credo_naming is a separate hex package). Cost: version drift between TLX internals and check implementations. Checks need access to the same DSL introspection and emitter derivation logic the runtime uses; if they live in a separate repo, every TLX internal change risks silently breaking checks that were correct at the time of writing.
  • Default-on checks. Maximally prescriptive. Cost: violates ADR-0014's premise that enforcement is project policy, not transpiler policy. Forces every TLX consumer to either follow the conventions or explicitly disable checks they didn't ask for.
  • Custom :formality category. Considered and rejected: Credo enumerates :consistency, :design, :readability, :refactor, :warning as the valid category atoms, and the exit-status mapping plus CLI selection is hardcoded to that set. A non-standard category would fragment the UX without earning anything; tags are the supported extension mechanism.

Decision

TLX ships a Credo plugin under TLX.Credo.Check.*, bundled with the TLX library, default off, registered via .credo.exs at the consuming project's discretion.

Packaging. Checks live in lib/tlx/credo/check/ within the TLX repository. They are version-locked with TLX internals because they depend on DSL introspection and emitter derivation logic. There is no separate tlx_credo package on Hex.

Discovery. Consumers register checks in their .credo.exs:

%{configs: [%{checks: %{enabled: [
  {TLX.Credo.Check.ExplicitConstants, []},
  {TLX.Credo.Check.NestingDepth, []},
]}}]}

No auto-loading. The Credo requires mechanism is reserved for project-local checks.

Default state. All checks ship disabled. Enabling is an opt-in act per project, consistent with ADR-0014's principle that enforcement is project policy.

Categorization. Checks use Credo's standard categories: :readability for stylistic recommendations, :warning for real bug classes. The grouping mechanism is the :tags field, with two tags reserved:

  • :tlx — every TLX-provided check carries this tag. Lets users select all TLX checks via mix credo --checks-with-tag tlx.
  • :tla_formality — checks that recommend the explicit-form Layer 3 enforcement from ADR-0014. Distinguishes "make this look like a TLA+ veteran wrote it" checks from checks targeting genuine bug classes.

Initial check set. Two checks ship in the first cut:

  • TLX.Credo.Check.ExplicitConstants — category :readability, tags [:tlx, :tla_formality]. Flags specs that rely on auto-derived CONSTANTS instead of declaring them explicitly via the DSL's explicit form (Layer 1 of ADR-0014). Necessarily downstream of the DSL surface that introduces explicit CONSTANTS declarations — the check can be defined now but only fires once that surface lands.
  • TLX.Credo.Check.NestingDepth — category :warning, tag [:tlx]. Flags DSL nesting that reaches three levels (e.g. process > action > branch), which triggers a non-fatal FunctionClauseError warning in Spark 2.6. Independent of any DSL surface change; can land immediately.

A third check, identifier naming conventions (mapping Elixir atom case to idiomatic TLA+ symbol case), is anticipated but its DSL surface and convention boundaries are not yet settled. It is excluded from the initial set and will land when its scope is clear.

Scope boundary. This ADR establishes the packaging architecture and the initial check set. Future checks following the same pattern (standard category, :tlx tag, opt-in registration) can be added without a new ADR. A new ADR is required only if the architecture changes — for example, if checks need to be split into a separate package, if categorization conventions shift, or if a default-on policy is reconsidered.

Consequences

Positive:

  • Layer 3 of ADR-0014 has a concrete implementation path.
  • Bundling avoids version drift between checks and the TLX internals they introspect.
  • Standard categories + tags compose with existing Credo workflows: mix credo --only readability includes TLX checks, mix credo --checks-with-tag tla_formality runs just the formality subset.
  • Default-off respects ADR-0014's policy boundary: TLX provides the tools, the project decides what to enforce.
  • Consumers writing throwaway specs pay zero cost — disabled checks don't run.

Negative:

  • Adds a hex dep on Credo for TLX. Could be mitigated by making it optional: true in mix.exs, with checks compiled only when Credo is present in the consuming project.
  • Bundling means TLX's published package grows. Marginal — checks are small Elixir modules.
  • The :tla_formality tag is a TLX-coined convention. If a future Credo plugin from another author wants similar grouping, there is no shared registry; tags are inherently namespace-free.

References

  • ADR-0014 — establishes Layer 3 as the home for prescriptive enforcement
  • ADR-0007 — the auto-derivation behavior ExplicitConstants is opt-in counterpart to
  • Credo: Adding Custom Checks — plugin authoring conventions
  • lib/tlx/credo/check/ — implementation (forthcoming)