lambdaclasstrzk

Verified Optimizing Compiler for Cryptographic Primitives
Sort by
  1. Git dependency.
    Found on Reservoir.

    mathlibv4.26.0

    The math library of Lean 4
  2. Git dependency.
    Found on Reservoir.

    optisat0439a64

    Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems