Reference

Verified core

The Lux compiler front-end carries two layers of verification beyond its unit suite: machine-checked proofs over bounded domains, and property tests over generated inputs. This page is extracted from those source files at every site build — it is a view of the artifacts, not a description of them.

extracted from crates/lux-lang/src/ · 9 proofs · 50 properties · build 2026-06-29

Kani proofs

Bounded model checking: each harness exhaustively explores its stated domain — every input in the bound, not a sample. What it guarantees is exactly the property over exactly that domain, no more.

run: cargo kani -p lux-lang

escape is invertible for all printable ASCII characters.

For every byte 0x20..=0x7E, escape → unescape produces the original.

prove_escape_roundtrip_printable_ascii

escape is invertible for all control characters (0x00..0x1F).

prove_escape_roundtrip_control_chars

escape never produces an unquoted double-quote.

The escaped output must not contain a bare `"` (which would break string literals).

prove_escape_no_bare_quote

escape never produces an unquoted newline.

Newlines in the output would break the string literal across lines.

prove_escape_no_bare_newline

escape output length is >= input length.

Escaping can only grow or maintain size, never shrink.

prove_escape_length_monotonic

escape is idempotent on already-safe characters.

For characters that don't need escaping (alphanumeric, space, punctuation excluding `\`, `"`, `{`), the output equals the input.

prove_escape_identity_safe_chars

escape roundtrip for DEL (0x7F) character.

DEL is a control character despite being above 0x1F.

prove_escape_del_char

indent stack is always monotonically increasing.

Simulates the indentation state machine over bounded inputs. The indent_stack must maintain the invariant: each element > previous.

prove_indent_stack_monotonic

indent stack always starts with 0.

The base indent level must always be 0, no matter what sequence of indent/dedent operations occur.

prove_indent_stack_base_zero

Property invariants

Property-based testing: each invariant is checked against randomized generated inputs (256 cases per run by default) plus every previously-found failing seed. Weaker than a proof — it samples the domain — but it covers domains too large to bound.

run: cargo test -p lux-lang proptest

P1	Roundtrip idempotency for generated modules	prop_roundtrip_idempotent
P2	Tokenize never panics for arbitrary strings	prop_tokenize_never_panics
P3	Parse never panics for arbitrary strings	prop_parse_never_panics
P4	Nesting depth limit prevents stack overflow	prop_nesting_depth_limit
P5	All keywords tokenize correctly	prop_keywords_tokenize
P6	Item count preserved through roundtrip	prop_item_count_preserved
P7	Integer literals survive roundtrip	prop_int_literal_roundtrip
P8	Binary operator associativity is stable	prop_binop_associativity
P9	Simple string literals survive roundtrip	prop_string_literal_roundtrip
P10	List literals survive roundtrip	prop_list_literal_roundtrip
P11	Indentation with consistent spaces produces valid tokens	prop_indent_consistent_spaces
P12	Dedent back to column 0 produces matching dedent tokens	prop_indent_dedent_balanced
P13	Invalid dedent level produces an error	prop_invalid_dedent_error
P14	String escape sequences roundtrip correctly	prop_string_escape_roundtrip
P15	Unicode escape sequences tokenize without panic	prop_unicode_escape_no_panic
P16	Integer overflow produces error, not panic	prop_int_overflow_error
P17	Float literals with varying decimal places roundtrip	prop_float_literal_roundtrip
P18	Empty string roundtrips	prop_empty_string_roundtrip
P19	Comments are stripped by lexer (don't appear in AST)	prop_comments_stripped
P20	Multiple blank lines between items don't change AST	prop_blank_lines_ignored
P21	All binary operators produce stable roundtrips	prop_all_binops_roundtrip
P22	Logical operators roundtrip	prop_logical_ops_roundtrip
P23	If/else statement roundtrip	prop_if_else_roundtrip
P24	For loop roundtrip	prop_for_loop_roundtrip
P25	While loop roundtrip	prop_while_loop_roundtrip
P26	Match statement roundtrip	prop_match_roundtrip
P27	Nested function definitions roundtrip	prop_nested_func_roundtrip
P28	Record literal roundtrip	prop_record_roundtrip
P29	Lambda expression roundtrip	prop_lambda_roundtrip
P30	Pipe operator roundtrip	prop_pipe_roundtrip
P31	Strings with newlines roundtrip correctly (escape bug regression)	prop_string_with_newline_roundtrip
P32	Strings with tabs roundtrip correctly	prop_string_with_tab_roundtrip
P33	Strings with null bytes roundtrip correctly	prop_string_with_null_roundtrip
P34	Strings with escaped braces roundtrip	prop_string_with_brace_roundtrip
P35	Strings with backslash roundtrip	prop_string_with_backslash_roundtrip
P36	Strings with quotes roundtrip	prop_string_with_quotes_roundtrip
P37	Mixed escape sequences in one string roundtrip	prop_mixed_escapes_roundtrip
P38	Boolean roundtrips	prop_bool_roundtrip
P39	Range expressions roundtrip	prop_range_roundtrip
P40	Unary operators roundtrip	prop_unary_roundtrip
P41	Field access chains roundtrip	prop_field_access_roundtrip
P42	Function calls with arguments roundtrip	prop_call_roundtrip
P43	Index expressions roundtrip	prop_index_roundtrip
P44	Return statement roundtrip	prop_return_roundtrip
P45	Unless statement roundtrip (Ruby-style)	prop_unless_roundtrip
P46	Until loop roundtrip (Ruby-style)	prop_until_roundtrip
P47	Null coalesce operator roundtrip	prop_null_coalesce_roundtrip
P48	String interpolation roundtrip	prop_interpolation_roundtrip
P49	Signal expression roundtrip	prop_signal_roundtrip
P50	Memo expression roundtrip	prop_memo_roundtrip

What this does and doesn't claim

Proofs hold over their stated bounded domains — e.g. all printable ASCII, not all of Unicode.
Property tests sample; a passing run is evidence, not proof.
Coverage is the compiler front-end (lexer, parser, printer). The evaluator and runtime are covered by their unit suites, not by these artifacts.
This page regenerates from the source files at every site build. A claim listed here exists in the code on the build date shown above.

Determinism is gated separately: every compiler emit surface is byte-deterministic and checked in CI (see format and check in CI).