Popular repositories Loading

1. CatCrypt-core CatCrypt-core Public

   Core of Catcrypt

   Lean 9 5

2. libcrux-lean-specs libcrux-lean-specs Public

   Hax Lean 4 prelude for libcrux pure crypto specs

   Lean 5 1

3. hax-lean hax-lean Public

   Verified hax compiler phases in Lean 4: AST, semantics, 4 phases, end-to-end pipeline correctness

   Lean 3 1

4. ParamTransfer ParamTransfer Public

   Relational proof transfer in Lean 4 — a confluence of parametricity (Trocq), congruence closure, functorial casts (AdapTT), and data refinement (CoqEAL).

   Lean 2 1

5. nominal-lean nominal-lean Public

   Lean 2

6. Divided-Difference Divided-Difference Public

   Paper and formalization on divided differences

   1