ALS — the Almide Language Specification

What an Almide implementation is judged against. This repository holds the language's normative semantics, its behavior-contract ledger, the executable conformance corpus, the traceability gates that bind those three together, and a runner that executes the corpus against any almide binary. It holds no compiler.

Almide's mission is to be the language LLMs write most accurately, and its declared quality bar is aviation-grade (DO-178C-class). At that bar the requirements and the verification evidence are configuration-managed independently of the implementation, with two-way traceability between them; a requirement is reviewed before the code that satisfies it, and the verification suite must be runnable by someone who did not write the compiler. This repository is that independence made structural. It is to almide/almide what ferrocene/specification is to the Ferrocene compiler, what seL4/l4v is to the seL4 kernel, and what WebAssembly/spec is to every wasm engine.

The Almide organisation already has one external judge — almide/almide-dojo measures LLM writability (modification survival rate) from outside the compiler. ALS is the second judge: correctness.

What is here

Path	Role
docs/specs/als/	Normative semantics (## ALS-<id> sections). Every section is cited by ≥1 contract; every contract cites a section — both directions gated.
docs/specs/*.md	Language specification chapters: language, type system, effect system, modules, packages, Result/Option/effect, effect-fn call semantics, edit locality.
docs/SPEC.md, docs/GRAMMAR.md, docs/design/	Design thesis, EBNF grammar, design doctrine (equivalence, hidden operations, rejected patterns).
docs/adr/	Architecture Decision Records — the why behind the language decisions, with falsifiers.
docs/contracts/contracts.toml	Behavior-contract ledger: 301 named C-NNN promises (stdout, stderr, exit code — identical on every target). README.md and conformance.md next to it are generated from it.
spec/wasm_cross/	591 cross-target fixtures, each declaring the contract(s) it certifies on a // @contract: header. The ledger ↔ fixture link is symmetric and gated.
spec/lang/, spec/stdlib/, spec/integration/	Test-block corpora (almide test) — language, stdlib, multi-module.
spec/wasm_fail/, spec/programs/, spec/wasm_cross_pkg/	Failure-shape fixtures (// @expect-fail:), whole programs, the package-form cross-target fixture.
tests/diagnostics/	752 diagnostic cases (broken.almd must be rejected with the pinned code/hint; fixed.almd must compile). Rejection behaviour is part of the language surface.
proofs/als-element-coverage.toml	Every surface-syntax element → the ALS section that specifies it (72/72 sectioned, 0 UNWRITTEN — a freeze precondition).
proofs/contract-provenance.toml	Every contract → the instant its id entered the ledger vs the instant its since release was tagged: requirements-first / contemporaneous / retroactive (shrink-only) / unmeasured. The two-PR order, measured.
proofs/als-validation.toml	Per-section validation record (who reviewed which ALS-<id>, when, independently or not, with what verdict), bound to a hash of the section text; unvalidated sections are a shrink-only ceiling.
proofs/runner-coverage.toml	How much of the runner its self-test exercises: line coverage of scripts/conformance.py under the 21 scenarios, an exact floor (line, not branch; the uncovered lines are listed).
proofs/dialect-epochs.toml	The dialect-epoch record: what each epoch added, deprecated, removed.
scripts/check-contracts.sh	Contract-ledger traceability gate (schema, evidence floor, symmetric links, spec keying, generated-doc freshness, retired-path citations).
scripts/check-als-element-coverage.sh	Element-coverage gate (ledger side here; AST enumeration with an implementation root).
scripts/check-contract-provenance.py	Provenance gate: every contract classified, classes derived from the recorded instants (a hand-edited class fails), retroactive count pinned to a shrink-only ceiling. --write regenerates from history.
scripts/check-als-validation.sh	Validation-record gate: a review outlives only the exact text it covered (hash-bound, STALE otherwise); --stamp ALS-<id> prints a row skeleton.
scripts/check-runner-coverage.py	Runs the self-test with the runner's stdlib trace hook on and compares the measured line coverage with the recorded floor (below = regression, above = ratchet up).
scripts/check-ratchet-separation.sh	A ratchet loosening (ceiling up, floor down in proofs/*.toml) must be its own commit with a dated justification — the change that needed it cannot move the baseline silently (lefthook on the staged diff, CI over the PR's commits).
scripts/conformance.py	The runner. Executes the corpus against a binary and writes a conformance statement.
ref/	The reference evaluator (ADR-0015): a fresh, source-level evaluator of Almide programs in pinned stable Rust (Ferrocene-tracking), zero dependencies, no almide-* crate — the judge's own reading of the ALS text, behind the protocol als-ref run <file> --json.
proofs/kernel-conformance/	The λ_almd kernel corpus (48 generated programs + the nine-line kAll trace, evaluator-pinned by the Lean belt; PROVENANCE.toml) — the reference evaluator's seed oracle, held at agreement 1.0.
proofs/ref-abstain.toml	What the reference evaluator does not evaluate yet, by class, over spec/wasm_cross + spec/programs — shrink-only.
scripts/check-ref-kernel.py, scripts/check-ref-independence.sh, scripts/check-ref-totality.py	The evaluator's gates: kernel agreement 1.0 twice (determinism); no almide-* dependency, pinned stable channel, clippy clauses (forbidden host types/methods), F64 without Display, rustfmt; totality-or-abstain and the shrink-only abstain ledger.
BOUNDARY.md	The classification of every path that was and was not moved here, with rationale, and the provenance of the extraction.

Paths are kept verbatim from the implementation's layout on purpose: the ledger, the fixtures, the ALS prose and the implementation's own gates all cite them, and a pinned checkout of this repository must be diffable against the copies the implementations still carry.

How an implementation uses this repository

1. Pin a commit (later: a tag) of almide/als.
2. Run the gates with an implementation root so implementation-resident evidence (cargo gates, Lean theorems, proofs/*.v) is required to exist:

   bash scripts/check-contracts.sh            --impl-root /path/to/almide
   bash scripts/check-als-element-coverage.sh --impl-root /path/to/almide

   Without a root, those paths are counted and reported as deferred — never silently passed, never falsely red. Judge-resident evidence is required unconditionally.
3. Run the judge against the built binary (wasmtime on PATH):

   python3 scripts/conformance.py --almide /path/to/almide --report conformance.toml

   The statement records the ALS commit, the binary's version, the platform, the legs and any --limit, and per-leg counts with every failure verbatim. A verdict is only as wide as what the statement says was run.

Change discipline (requirements first)

• A behaviour change lands here before it lands in an implementation. New behaviour = a new C-NNN contract citing its ALS-<id> section + ≥1 fixture declaring it, in one PR to this repository. The implementation then bumps its pin and makes the judge pass — a second, separately reviewed PR. The git history of the two repositories is the evidence that requirements preceded code, and proofs/contract-provenance.toml measures it per contract (the retroactive count may only shrink).
• Fixture headers: // @contract: C-NNN[, C-MMM] (mandatory in spec/wasm_cross), // @xt-allow: <reason + ref> (a known, tracked divergence — logged, and flagged stale the moment it heals), // @expect-fail: <stderr substring> and // @xf-allow: in spec/wasm_fail.
• Contract ids are contiguous; since is the release the behaviour became normative; the flagged-for-revision count is a ratchet that may only go down (current ceiling: 0).
• Derived documents are regenerated, never edited: bash docs/contracts/generate-readme.sh > docs/contracts/README.md and bash docs/contracts/generate-conformance.sh > docs/contracts/conformance.md.
• Decisions with alternatives get an ADR (docs/adr/README.md has the form).

Versioning

main is the only long-lived branch; it accepts pull requests that pass the gates workflow. A tag is an edition of the specification and is what implementations pin. The first tag is the semantics freeze (almide/almide roadmap item A0-1, sequenced after ADR-0012 D2/D3) — until then, implementations pin a commit SHA. A tag never moves.

Provenance

Extracted from almide/almide at commit 53e2a2ab7 (branch develop, 2026-08-20) with git filter-repo, keeping the full history of every path listed in BOUNDARY.md — 1,321 commits. Earlier history of paths that were renamed into place lives in the implementation repository.

Honest status

• The ALS normative text covers stdlib and observable semantics section by section; there is no mechanized evaluation relation for Almide source here yet. proofs/ALS.v in almide/almide is the implementation's ownership checker model (it imports OwnershipChecker) and stays there; a language-level mechanized semantics, when written, belongs here. The executable reading exists since 2026-08-21: ref/ reproduces the λ_almd kernel corpus 49/49 and, over spec/wasm_cross + spec/programs, evaluates 173 of 602 programs (171 of the 172 comparable ones agree with the native target; the one disagreement and the two findings are in docs/ref/PARSER-NOTES.md) and abstains on 429 in 152 ledgered classes — the long tail is stdlib. The runner's ref leg exists (verdict legs == ref wherever the reference evaluates; abstains counted, never verdicts; // @ref-allow: tracks adjudicated findings) — so limitation 2 of QUALIFICATION.md is now bounded by the abstain ledger instead of by the absence of an instrument: on the evaluated subset the runner judges truth, on the abstained subset it still judges agreement.
• The greenfield rebuild pins this repository as a submodule since 2026-08-20 (BOUNDARY.md, "Stage B"); almide/almide develop still carries copies, and its cutover is a separately decided step.
• docs/stdlib/ (the per-module API reference) and docs/CHEATSHEET.md remain in the implementation pending classification; both are partly generated from compiler source today.

License

Dual-licensed under MIT or Apache-2.0, the same terms as almide/almide (LICENSE, LICENSE-MIT, LICENSE-APACHE).