Verbatim clone of integritychain/fips205 (pure-Rust FIPS 205 / SLH-DSA), pinned at 30bac08 for the SLH-DSA formal-verification campaign. Aeneas-compat patches land here as transparent commits. Independent snapshot: no affiliation with, and no changes prop
Updated 2026-09-04 03:00:03 +00:00
Proof-aware crypto tooling evidence interpreter and risk scorer
Updated 2026-08-22 19:18:01 +00:00
Updated 2026-08-22 16:43:06 +00:00
Formally verified ed25519 (betrusted-io curve25519-dalek fork v4.1.2, Precursor/Xous): field + complete Edwards addition law proven in Lean 4 via Charon/Aeneas; axiom-audited certificates
Updated 2026-08-22 16:43:05 +00:00
Formally verified ed25519 (risc0 curve25519-dalek fork v4.1.3): field + complete Edwards addition law proven in Lean 4 via Charon/Aeneas; axiom-audited certificates
Updated 2026-08-22 16:43:03 +00:00
Formally verified ed25519 (anza-xyz solana-ed25519): field + complete Edwards addition law proven in Lean 4 via Charon/Aeneas; axiom-audited certificates
Updated 2026-08-22 16:43:02 +00:00
Formally verified ed25519 (upstream curve25519-dalek v5): field + complete Edwards addition law proven in Lean 4 via Charon/Aeneas; axiom-audited certificates
Updated 2026-08-22 16:43:00 +00:00
A hands-on undergraduate curriculum: formal verification of real cryptographic code with Lean 4 — companion to the *-ed25519-verified and pasta-pallas-verified projects
Updated 2026-08-22 16:42:29 +00:00
Git-published Lean formal-verification transparency log: attestations, Merkle inclusion receipts, signed tree heads (dogfood-signed by the proof-attested Ed25519 library), and a stdlib-only standalone verifier.
Updated 2026-08-22 16:41:44 +00:00
Machine-checked verification campaign for the SLH-DSA (FIPS 205) verify path: Rust (fips205-source) -> Charon/Aeneas -> Lean 4. Parameter set SLH-DSA-SHA2-128s first. STATUS: skeleton - nothing proven yet.
Updated 2026-08-16 16:32:40 +00:00
Formally verifying Pallas (zcash/pasta_curves) field arithmetic in Lean 4 via Charon/Aeneas — real extraction, no bridge axioms; field layer under construction, group law + scalar mul planned
Updated 2026-08-07 14:00:54 +00:00
Updated 2026-07-07 17:17:39 +00:00
Patched source for Aeneas/Charon formal verification transpilation
Updated 2026-07-05 23:41:56 +00:00
Patched source for Aeneas/Charon formal verification transpilation
Updated 2026-07-05 23:41:55 +00:00
Patched source for Aeneas/Charon formal verification transpilation
Updated 2026-07-05 23:41:54 +00:00
Patched source for Aeneas/Charon formal verification transpilation
Updated 2026-07-05 15:40:43 +00:00
Pasta curves (Pallas/Vesta) — formal verification source
Updated 2026-07-02 14:53:27 +00:00