Radix は整数、ビット、バイト列、メモリ、バイナリ形式、並行性、ベアメタル支援までを含む Lean 4 向けの低レイヤー基盤ライブラリです。zero sorry、proof-erased abstractions、named trust assumptions を軸に、仕様と実装の境界を明示的に管理しています。

• Word / Bit / Bytes / Memory / Binary / Concurrency / BareMetal をまたぐ低レイヤープリミティブを整理。
• Proof-erased abstractions によって検証成果をランタイムコストへ持ち込まない。
• Lean 4 kernel + Mathlib + named trust assumptions という信頼境界を明示する。

WebAssembly の数値セマンティクス、128-bit SIMD、線形メモリを Lean 4 で形式化し、定義・実装・証明を一体として伸ばしているプロジェクトです。Wasm runtime の正しさを説明可能にするための土台として進めています。

• WebAssembly numeric semantics を Lean 4 上で定義し、モデルのズレを証明可能にする。
• 128-bit SIMD と linear memory まで含めて検証対象を拡張する。
• 実装・定義・証明を分断せずに前進させ、ランタイム周辺の理解を固める。