Boolean-kernel basis: native evaluation-form FRI folding, a multilinear PCS, post-quantum security, Lean 4 formalisation (no sorry)

Kronecker-FRI: hash-based multilinear polynomial commitment from a coefficient-extraction identity — paper, proofs, Rust

Bilingual reconstruction, Lean formalization, and Rust experiments for a 2005–2006 finite-group representation theory research project.

Taking the Zerocash construction apart clause by clause — a 2014 seminar study reconstructed, plus a Rust implementation whose tests prove each constraint necessary.

Mersenne-31 kernel-basis experiments and STWO parity/reproducibility artifacts.

Rust and SystemVerilog tree-based polynomial evaluation over Mersenne-31 with parallel FPGA implementations.

Mersenne-31 FPGA Sumcheck prover with RTL, software cross-checking, synthesis and board validation.

Lean 4 formalization of delegated AI-agent authorization and protected-tool execution.

Lean + executable semantic validation of OpenVM RV64 native-recompiler word operations

KSTARK Hybrid — Rust kernel-basis global-linear proofs composed with binary-field nonlinear reductions and FRI, by Algorizk Labs.

Boolean zeta transform, kernel-polynomial degree filtration, M31 domain-tower FFT and Circle-FFT rescaling with Rust/ARM64 reproducibility.

Algorizk Labs research on finite-field AES representations and reproducible cryptanalytic time-memory tradeoffs in Java and Rust.

Boolean kernel polynomial basis and its low-degree filtration — paper, Lean formalization, and Rust implementation

Basis-aware multilinear polynomial algorithms and the Sumcheck protocol in Rust

Ariadne 001 — public research, formal contract, and software-level verification artifact

Research and engineering in cryptography, verifiable computation, mathematical computing and hardware acceleration.

Thaler-book-exercices