The CeeSafe Specification

CeeSafe is a memory-safe systems programming language with C#/TypeScript-style syntax, compiled ahead of time to portable C. This directory is its specification. ceesafec embeds it: ceesafec explain and the MCP server (ceesafe_spec_search, ceesafe_spec_section, the ceesafe://docs/… resources) serve this text.

CeeSafe forked from Nova at Nova v0.6.0, when the two were the same language (CeeSafe's Decisions 0003 and 0006 in the repository's docs/decisions/). This text began as Nova's specification at that tag, renamed and changed where the fork changed something (§3). From the fork on it is CeeSafe's own: Nova's later changes do not apply to it, and its changes do not apply to Nova.

1. Documents

Normative, in order of authority after the ADRs:

Document	What it specifies
decisions/	the ADRs: accepted decisions override the other documents' proposals (§2)
ownership.md	the safety invariants (O*, B*, E*, R*, H*, U*) and their formal design
language-spec.md	the language: goals, syntax overview, semantics
grammar.md	the grammar
type-system.md	types and static semantics, the built-in types and libraries, chapter by chapter
lifetimes.md	references and the borrow checker
memory-model.md	allocation, regions, placement
unsafe.md	unsafe, raw pointers and their contract
c-backend.md	the generated C: its rules, names, ABI version, structure
optimisations.md	each optimisation's preconditions and checks
profiles.md	the hosted and freestanding profiles and their runtimes
diagnostics.md	every diagnostic code
tooling.md	the command line, doc, lsp, debugging, packages, fixes, explain, mcp, agent files
formatting.md	the canonical style ceesafec fmt writes
api/core.md	lib/core's API, generated by ceesafec doc

Descriptive: architecture.md (how ceesafec is built), intermediate-representation.md (the AST, HIR and NIR as implemented) and testing.md (how CeeSafe is tested).

The guide teaches the language; every example in it is compiled by tools/guide_check.py. Both are published at vkuttyp.github.io/CeeSafe (the repository's site/).

2. Decisions

decisions/0001–0030 are Nova's ADRs, inherited at the fork. Their text is Nova's record, unchanged, under a header that says so. CeeSafe's own language decisions continue the series from ADR 0031 in the same directory. The port's decisions (how CeeSafe was made from Nova: names, bootstrap, the fork point) are "Decisions" in the repository's docs/decisions/, a separate series.

3. What the fork changed

At the fork the language is Nova v0.6.0's; what differs is how it is named and built:

• the compiler is ceesafec; source files are .cee; packages are ceesafe.toml and ceesafe.lock, the cache is $CEESAFE_HOME (default ~/.ceesafe), and the default registry index is github.com/vkuttyp/CeeSafe-index;
• the command line reads only .cee and .c files (tooling.md);
• the generated C and the runtime use CeeSafe's names: cee_, ceeF_, ceeMk_, … for generated names, and ceesafe_*, CEE_*, CEESAFE_*, ceesafe/rt.h for the runtime; programs may not declare C names with those prefixes (N0292); and ceesafe/rt.h defines CEESAFE_ABI_VERSION, which every generated unit checks (c-backend.md §1.1);
• messages say CeeSafe: ceesafe panic: ….

4. Reading this text

• Milestone tags (M1–M15, C0–C9, K1–K7, G7b, …) name the Nova milestone that introduced a rule. They are kept so a rule can be traced to Nova's history; they say nothing about CeeSafe's plan.
• Links to Nova. A document CeeSafe did not fork (Nova's milestones, roadmap, open decisions, reports, research) is linked in Nova's repository at v0.6.0.
• CosmoOS. The kernel profile, lib/kernel and the CosmoOS bindings were developed by Nova inside CosmoOS, and CosmoOS builds its Nova code with novac. Where this text reports what was run in CosmoOS, it was run with Nova.
• Paths. src/… is ceesafec's source. lib/… and runtime/… name the library and runtime sources ceesafec embeds, CeeSafe's own since Decisions 0007 and 0008 (architecture.md §6). tests/corpus/…, benchmarks/… and programs/… are CeeSafe's copies under tests/reference/ (Nova's at the fork, as .cee files). integrations/cosmoos/… is CeeSafe's own adaptation of Nova's CosmoOS checks (testing.md §1).
• Tests. A test named like a C# class (FixTests, PlacementTests) is Nova's; where CeeSafe has its own check, the text names its tool (testing.md).

5. Changing it

Spec before code: a change to the language changes this specification first, with an ADR when it is a decision, and then the compiler, its tests and the guide. Each change that makes CeeSafe differ from novac 0.6.0 is recorded as an exception in the comparisons (testing.md §3).