Skip to content
@Verilean

Verilean

Shedding light on silicon with formal verification. Powered by Lean 4. Home of Sparkle HDL and Hesper Inference Engine.

Popular repositories Loading

  1. sparkle sparkle Public

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

    Lean 38 4

  2. hesper 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 prova…

    Lean 15 1

  3. gungnir-operator gungnir-operator Public

    Formally Verified Valkey Operator

    Lean 3

  4. xeus-lean xeus-lean Public

    Lean

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
    Lean 38 Apache-2.0 4 1 0 Updated Mar 22, 2026
  • 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
    Lean 15 Apache-2.0 1 0 0 Updated Feb 19, 2026
  • xeus-lean Public
    Verilean/xeus-lean’s past year of commit activity
    Lean 0 0 0 0 Updated Feb 15, 2026
  • gungnir-operator Public

    Formally Verified Valkey Operator

    Verilean/gungnir-operator’s past year of commit activity
    Lean 3 0 0 0 Updated Feb 15, 2026

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…