Implementation of various cryptographic functions in Lean4

Verified GPU programming framework for Lean 4. Write type-safe WebGPU shaders with formal verification, hardware-accelerated matrix ops, and cross-platform support (Metal/Vulkan/D3D12). Build provably correct GPU compute and ML inference engines.

a zero-knowledge proof-carrying code platform for Lean 4

(Mirror) A Machine-to-Machine Interaction System for Lean 4

Low level utils (single precision float, byte spans, unboxed vector, finalization callbacks, fixnums, deque, slotmap etc; implemented via ffi)

Raylib bindings for Lean4

Lean bindings for redis/hiredis

A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.