Verilean
Shedding light on silicon with formal verification. Powered by Lean 4. Home of Sparkle HDL and Hesper Inference Engine.
Pinned Loading
Repositories
Showing 4 of 4 repositories
- sparkle Public
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
Verilean/sparkle’s past year of commit activity - xeus-lean Public
Verilean/xeus-lean’s past year of commit activity - hesper Public
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.
Verilean/hesper’s past year of commit activity
People
This organization has no public members. You must be a member to see who’s a part of this organization.
Top languages
Loading…
Most used topics
Loading…