Lean Toolchain

Cryptographic, math, and data-parsing primitives formally proven in Lean 4.

Overview

Lean Toolchain provides a collection of formally verified cryptographic algorithms, mathematical operations, and data parsing utilities. All implementations are proven correct in Lean 4 and can be extracted to high-performance Rust code.

Key Features

• Formally Verified: All algorithms come with mathematical proofs of correctness
• High Performance: Extracted Rust code matches or exceeds industry standards
• Comprehensive: SHA-256, HMAC, linear algebra, CSV/JSON parsing
• Developer Friendly: Clear documentation, examples, and contribution guidelines

Quick Start

Prerequisites

• Lean 4
• Rust (for extraction)

Installation

# Clone the repository
git clone https://github.com/SentinelOps-CI/lean-toolchain.git
cd lean-toolchain

# Build the project
lake build

# Run tests
lake test

Usage

import LeanToolchain.Crypto.SHA256
import LeanToolchain.Math.Vector

-- SHA-256 hashing
#eval sha256 "hello world"

-- Vector operations
#eval Vec.cons 1 (Vec.cons 2 Vec.nil)

Project Structure

lean-toolchain/
├── LeanToolchain/           # Main library
│   ├── Crypto/             # Cryptographic primitives
│   ├── Math/               # Mathematical operations
│   └── Data/               # Data parsing utilities
├── docs/                   # Documentation
├── bench/                  # Benchmarks
└── scripts/                # Build and release scripts

Development

Running Tests

lake test

Building Documentation

# Install mkdocs-material
pip install mkdocs-material

# Build docs
mkdocs build

Contributing

We welcome contributions! Please see our Contributing Guide and Development Documentation for details.

Documentation

• API Reference
• Examples
• Development Guide

License

This project is licensed under the MIT License - see the LICENSE file for details.

Acknowledgments

• Lean 4 - The theorem prover and programming language
• RustCrypto - For reference implementations
• NIST - For cryptographic test vectors