qssl 0.2.0

Pure Rust post-quantum TLS — zero C code. ML-KEM, ML-DSA, SLH-DSA, Falcon. FIPS 203/204/205/206 compliant. 100 Lean 4 theorems.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12

import Lake
open Lake DSL

package QSSLProofs where
  leanOptions := #[⟨`autoImplicit, false⟩]

@[default_target]
lean_lib QSSLProofs where
  srcDir := "."

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "v4.27.0"