Aether is an AI-native trustworthy systems-language research project. Its premise is that future code will primarily be generated by machines, while people define intent, responsibility boundaries, and audit requirements.
This repository currently contains the product requirements, the first executable K0 specification package, two independent semantic transition executors, and an evidence-backed implementation gate. It does not contain a production compiler and does not claim end-to-end verification.
- Specification version:
0.4.0-draft - Core layer:
K0 - G0 implementation gate: FAIL
- Authorized work: specification engineering and disposable semantic probes
- Production compiler: No-Go
The current executable subset covers move state, borrow conflicts, allocator brands, allocation failure, explicit deallocation, double-deallocation rejection, and affine leak diagnostics. Node and Python implementations agree on all 14 frozen transition vectors.
See the generated G0 report for the exact blockers and evidence.
| Path | Purpose |
|---|---|
docs/prd/ |
Historical product requirements, with v0.3 as the current parent PRD |
spec/ |
K0 constitution, grammar, ASR/Core contracts, rules, decisions, targets, and conformance corpus |
tools/ |
Independent Node/Python transition executors and offline validator |
reports/ |
Generated G0 status in human- and machine-readable forms |
experiment-log.md |
What was tested and learned while the project remains in lab/ |
Workspace scaffold directories (inputs/, outputs/, handoff/, and scripts/)
exist to preserve the enclosing AI-native lab protocol. They are not part of the
language specification.
Prerequisites are locked in spec/manifests/toolchain.json:
- Node.js
26.4.0 - Python
3.9.xat or above3.9.6(3.9.25in CI) - no external npm or Python packages
- no network access during validation
npm testValidation parses every JSON artifact, checks Rule ID and test links, runs both
executors, compares their canonical results, verifies target parameters, rebuilds
spec.lock, and regenerates the G0 report. A G0 FAIL is currently expected;
structural or semantic disagreement still makes the command fail.
- The implementation is not a source of language semantics.
- A semantic change requires an LCP, an immutable LDR, Rule ID changes, conformance evidence, compatibility analysis, and regenerated lock/report.
- K1/K2 features cannot enter the K0 route to make a test pass.
- Tests cannot create semantics; their oracle must cite an existing rule.
- AI output is untrusted until deterministic checks accept it.
Read CONTRIBUTING.md before changing normative material.
No public license has been granted. The repository is private research material until an explicit licensing decision is recorded.