A mechanised formal type theory based on extensional Martin–Löf type theory, checked by an elaborator/kernel pipeline: surface files elaborate to certificate-carrying artifacts that a small trusted kernel re-checks.
NovaFoundation, NovaSyntax, NovaModel, NovaKernel, NovaElaboration, NovaPipeline — the rules, rendered.
src/nova/*.nova, syntax-highlighted via the same semantic tokens the LSP sends an editor.
src/nova/*.nova