Issue #796: A formally verified compiler? Decision basis for using Nikaia’s proofs on the compiler itself

decision · opened 2026-10-24 · updated 2026-10-31 · 3 comments

How it came up

Owner’s question (2026-10-24): what would it take for Nikaia to call itself a formally verified compiler, by using the language’s own verification (asserts proved or refused with NK1300 under ADR-380, bounds and overflow proofs, struct rules, comptime, certificates under ADR-270) on the compiler’s own code as it moves into Nikaia (#125). The owner asked for a rough estimate and a feasibility class per requirement, not a build plan. Nothing concrete needs the answer now.

What was checked

Parts I-III of the specification are precise prose. There is no formal semantics: no formal grammar, typing judgements or operational rules. Part of a program’s meaning is defined by its lowering to Rust, and Rust has no complete formal semantics either.
The prover covers linear integer arithmetic with followed let mut, loop invariants, struct rules and preconditions. A small checker replays its certificates before a check is dropped. It does not cover an if used as a value, quantifiers, recursion or induction, strings, postconditions or termination. Probed on target/fast/nikaia.
Measured on the compiler’s own code with nikaia check --bounds, each of the 214 tools/*.nika files checked on its own: 1,473 indexes, 802 proved (54 %); 1,101 arithmetic steps, 491 proved (45 %). The code has 26 assert and 11 panic.

Decision basis

docs/formal-verification.md has the introduction, what the field means by the term (CompCert, CakeML, Vellvm, seL4, translation validation), the trusted base, and 17 requirements classed from A (reachable now) to E (probably never). In short:

Semantic preservation (CompCert’s claim): class D. It needs a formal semantics of Nikaia and of the Rust we write, plus a proof assistant. Removing rustc and LLVM from the trusted base is E.
Absence of run-time errors in the compiler’s Nikaia code (SPARK silver): class B. It needs prover extensions that every user gets too, and it can grow alongside the self-hosting moves.
Honest claims available now (A): the proved share of the compiler’s indexes and arithmetic, no unproved assert builds, every dropped check rests on a checked certificate, and Stage 1 agrees with the Rust stage on the suite.

Recommendation: do not aim at a verified compiler now. Aim at claim (b), and keep the door open with one cheap step.

First cheap step (needs no decision)

A Nikaia program scripts/proved.nika (run with nikaia run) that sums the --bounds and --asserts counts over crates/nikaia-std/src/tools/*.nika and prints one line. That line is recorded with each self-hosting snapshot. Test: its output on today’s tree gives the counts above.

For the owner

Is claim (b), a compiler whose Nikaia code is free of run-time errors, a goal, and if so, from when?
Should the name “formally verified” stay off the README and website until claim (a) exists?

Comments

keywan-ghadami, 2026-10-24

Owner’s answers, 2026-10-24 (recorded in docs/formal-verification.md section 6, commit 42ecccdc):

Claim (b) is the goal: the compiler’s Nikaia code proved free of run-time errors. The architect proposes it rides with stage 1, not after it.
“formally verified” is not written in README.md, on the website or in guide/ until semantic preservation (item 14) exists. The honest claims of section 4 may be used once they are true and measured.
Formal semantics: still open. The owner asked for more information first. The basis is docs/formal-semantics.md. It covers what a formal semantics is, three constructs (overflow on *, while, match) written as prose and as big-step rules, what the rules found straight away (the order operands are evaluated in is not stated, and the stop message comes from Rust), where the hard parts are (ownership, async, comptime), levels 0-4 from prose up to CompCert, risks, and a recommendation.

Correction to item 9: nikaia interpret evaluates nothing yet (Stage 0, it prints {}). A reference interpreter would be a new build.

To build (claim b)

scripts/proved.nika (run with nikaia run): for each tools/*.nika it runs nikaia check --bounds and adds up the proved and checked indexes and operations (asserts too, where check reports them). It prints one line in the same form as section 2’s figures (1,473 / 802; 1,101 / 491). Test: on today’s tree its totals match section 2, or the difference is explained.
The prover extensions as compiler work in the serial queue: #386 (products of unknowns), #432 (counters), #388 (lists of equal length).
The certificate checker (item 5) is the first file brought down to zero unproved checks.

The label stays decision while question 3 is open.

Generated by Claude Code

keywan-ghadami, 2026-10-24

Facts about data (owner’s follow-up, 2026-10-24): what the language can say today about lists and trees was probed (docs/facts-about-data.md). Today a pure bool property such as assert(is_sorted(v)) is allowed but refused (NK1300), or walked at run time at warn; struct rules over lengths are proved; nothing about elements can be stated. Step 1 is decided: ADR-381 (a named property is proved by name, carried to callers, published, checked once), built in #797 (ready). Rules over every element and std’s sorted contracts are the owner’s: #798 (decision). Correction to this issue’s basis: claim (b) needs no interpreter and no formal semantics (docs/formal-verification.md section 7); the reference interpreter stays an optional later stage.

Generated by Claude Code

keywan-ghadami, 2026-10-31

The owner set the target on 2026-10-31: 100 % of the checks in tools/*.nika proved (claim b). The work is tracked in #1053 (prover lane, docs/briefs/prover/). The figure measured today: 1,821 indexes, 965 proved; 1,381 operations, 560 proved. It counts each file on its own, and that undercounts, see #1053.

Generated by Claude Code

Back to Open Issues