Disclaimer: This project was mostly conjured by AI and has not been independently reviewed. Treat it as experimental research code.
BLS12-381 field arithmetic, G1 operations, compressed encoding/decoding, subgroup checks and pairing-product checks in Rust, extracted through Charon/Aeneas and proved against a pinned EthLib Lean specification. The Rust manually specializes arkworks 0.5.0 routines; tests compare outputs and instrumented intermediate states with the original crate.
Proofs establish termination and agreement with EthLib under each function's documented preconditions. Arkworks agreement is tested, not universally proved. Charon/Aeneas translation and native compilation remain trusted. The Rust is variable-time research code.
- Different exponentiation algorithms, one proved specification
- A small proved optimization
- Subgroup checks and point validation
- Pairing-product example and proof scope
Requires Rust, Lean, Python 3.11+, opam and native build tools; see setup and reproduction instructions.
cargo fetch --locked --manifest-path rust/Cargo.toml
make install-tools
make curveVerification includes 756 curve proof audits, 2,069 kernel-checked published
vector statements, native comparisons and instrumented Arkworks trace checks.
Reports and generated Lean are written to ignored build/ output. GitHub Actions
runs fresh extraction and verification for code changes.
Proof coverage · Arkworks adaptations · Verification audit · Pinned tools
Apache-2.0. Vendored sources and fixtures retain their third-party notices.