How Litex works
See how the software's parts work together, then follow individual statements as facts are checked, stored, inferred, and reused in later proofs.
The whole system
One component map. Knowledge that carries forward.
Choose the complete knowledge-building example or zoom into a definition, proof, reuse or computation. The fixed component map and detailed flow share one playback position.
Litex component map
Components stay in place; highlighted parts participate in this step.One file enters the system
The standalone file contains a definition, object declarations and facts. The component map shows the software's responsibilities before we follow any one statement.
Example source
Define is_less(x, y) as x < y. Name a = 2 and b = 5, then establish the predicate, read its inferred inequality, and reuse it with c = a and d = b.prop is_less(x, y R):
x < yhave a R = 2have b R = 5by def $is_less(a, b)a < bhave c R = ahave d R = b$is_less(c, d)Knowledge available to the next statement
No user knowledge has been committed yet.Checked failure boundaries
Replacing “have d R = b” with “have d R” leaves d arbitrary. The recorded run cannot establish $is_less(c, d); it returns a search miss with no stored or inferred effects for that statement.have d R{
"success": false,
"statement": "$is_less(c, d)",
"why_failed": {
"phase": "search_proof",
"goal": "$is_less(c, d)"
},
"stores": [],
"infers": []
}Detailed execution flow
The same example and playback position, expanded into its internal steps. Select a node to jump to its step; unused candidate routes show their explanation.Passed to the next part
The standalone file contains a definition, object declarations and facts. The component map shows the software's responsibilities before we follow any one statement.
Explore the atomic verification routes
An overview of checking an atomic fact: read the current knowledge, check that expressions are meaningful, and look for supported local grounds. Accepted facts extend the context; an unsuccessful check returns its stopping point while preserving earlier accepted knowledge.
Open original English diagramA note from the author
Litex from a Systems Engineering Perspective
Litex's central work is to develop a language and verification mechanism that can support everyday mathematical reasoning. Through experiments, refactoring, and real proofs, I have gradually shaped a system of objects (Obj), facts (Fact), and statements (Stmt), with mechanical checks for common relationships between them. These two lines show how those responsibilities meet:
Checked Litex source
have fn reciprocal(x R: x != 0) R = 1 / x
reciprocal(2) = 1 / 2The first line must establish a valid function before the second can use it. Inside the definition, x is a real number and x ≠ 0 is a local premise: it makes 1 / x meaningful and allows the body to be checked against the real return type. A successful declaration makes the named function, its restricted domain, and its defining equality available to later statements.
For reciprocal(2), the checker first establishes that 2 belongs to the input domain, including 2 ≠ 0. It can then use the recorded definition, substitute 2 for x, and justify the equality with 1 / 2. The condition belongs to the function's interface: every call must satisfy it, even though it was assumed locally while checking the definition.
Rejected at the input-condition check
reciprocal(0) = 0At zero, the required condition would be 0 ≠ 0. The call therefore fails its well-definedness check before Litex tries to establish the final equality; no fact is stored for this failed statement.
Objects (Obj) — represent expressions such as the function, 1 / x, and reciprocal(2), with the conditions under which they are meaningful.
Facts (Fact) — express membership, nonzero conditions, and equalities. Their evidence supplies the premises needed by object checks and later deductions.
Statements (Stmt) — organize definitions and checks in sequence, determine which scope a premise belongs to, and publish successful results for the next statement.
The difficulty is in the connections between these small steps. An ordinary fact can involve object domains, function guards, definition unfolding, equality substitution, rule premises, and scope at once. Each check may be elementary, but their interfaces must remain consistent as expressions and proof structures nest. Missing support can force authors to repeat mechanical steps; poorly organized verification can miss available evidence or spend unnecessary effort searching for it.
Litex evolves by finding these breaks in real mathematics, refining the expression model, filling missing relationships, and reorganizing verification. The aim is to let common steps compose under explicit premises and within controlled search boundaries. Authors still choose mathematical constructions and key proof routes; the language handles the mechanically checkable connections. A few readable source lines are the visible result of coordinating many such branches around shared mechanisms.
AI makes it possible for me to sustain this intensive design cycle with my own time and resources: propose an organization, implement it, test it on real proofs, and revise it when it fails. My work is to decide which classifications, relationships, and verification flows can work together over time; AI helps me implement, check, and repeatedly change the many details. Without that assistance, I would have found it difficult to explore and implement at a comparable intensity over roughly two years.