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 44 5

  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 20 1

  3. gungnir-operator gungnir-operator Public

    Formally Verified Valkey Operator

    Lean 4

  4. xeus-lean xeus-lean Public

    Lean 1

Repositories

Showing 4 of 4 repositories
  • 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 20 Apache-2.0 1 0 0 Updated Apr 6, 2026
  • 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 44 Apache-2.0 5 2 2 Updated Apr 3, 2026
  • xeus-lean Public
    Verilean/xeus-lean’s past year of commit activity
    Lean 1 0 0 0 Updated Mar 29, 2026
  • gungnir-operator Public

    Formally Verified Valkey Operator

    Verilean/gungnir-operator’s past year of commit activity
    Lean 4 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

Lean