Language: Z3 theorem prover embedded in the compiler. requires/ensures
contracts proved at compile time. Arena memory. MLIR codegen.

Compiler: 1,359 tests pass. 14 Z3 regression contracts. LLVM 21 compat.
Linux, macOS, Windows targets. Academic-level language specification.

Kernel: KeuOS microkernel boots in QEMU. TCP stack, SPSC rings,
SYN cookies with Z3-verified non-zero ISN. ECS architecture.

Lettuce: Verified Redis-compatible server. 7 modules. 4/4 Z3 contracts.

Docs: SPEC.md v4.0 (EBNF grammar, formal semantics), SYNTAX.md,
tutorial, FAQ, 3 blog posts, benchmark suite.