Work
Work
Rust verification with Lean, operating systems and compilers, CPU inference, and simulation. Each page states what exists and what remains.
Start with the results and evidence, the algebra, or memory safety and native-code verification.
-
Research · active
Apeiron
Rust algebra primitives with Lean proofs, tables, and a CPU inference engine.
Rust · Lean 4 · Aeneas · Charon · GGUF -
Research · active
Song
An operating system, language and compiler, with proof responsibility down to native instructions and bytes.
Iota · x86-64 · Lean 4 -
Research · active
Simulation
World generation, physical simulation and game systems on the same algebra.
Rust · Bevy · Luau
For collaboration, research funding or contract work, see contact details and areas of work.