Pure Lean 4 implementation of a TLS 1.3 client library. No C FFI or external dependencies (OpenSSL etc.).

• TLS 1.3 only (RFC 8446)
• Client only (no server implementation)
• Cipher suite: TLS_AES_128_GCM_SHA256
• Key exchange: X25519 (ECDHE)
• Certificate verification: RSA-PSS (rsa_pss_rsae_sha256) signature verification, hostname matching (SAN/CN)
• Toolchain: leanprover/lean4:v4.16.0

LeanTLS/
├── Crypto/
│   ├── SHA256.lean      # SHA-256 hash (FIPS 180-4)
│   ├── HMAC.lean        # HMAC-SHA-256 (RFC 2104)
│   ├── HKDF.lean        # HKDF Extract + Expand (RFC 5869)
│   ├── AES.lean         # AES-128 block cipher (FIPS 197)
│   ├── GCM.lean         # AES-128-GCM AEAD (NIST SP 800-38D)
│   ├── X25519.lean      # X25519 Diffie-Hellman (RFC 7748)
│   └── RSA.lean         # RSA-PSS signature verification (RFC 8017)
├── ASN1.lean            # ASN.1/DER parser
├── X509.lean            # X.509 certificate parser
├── CertVerify.lean      # TLS 1.3 certificate verification (RFC 8446 Section 4.4)
├── Record.lean          # TLS record layer (encrypt/decrypt)
├── Handshake.lean       # Handshake messages (ClientHello, ServerHello, Finished)
├── KeySchedule.lean     # TLS 1.3 key schedule (RFC 8446 Section 7.1)
└── Connection.lean      # High-level API: connect / send / recv / shutdown

Add to your lakefile.lean:

require «lean-tls» from git
  "https://github.com/kaito2/lean-tls.git" @ "main"

import LeanTLS

-- Wrap your TCP socket (or any transport) into an IOStream
let stream : LeanTLS.IOStream := {
  read := fun n => do /* read n bytes from socket */
  write := fun data => do /* write data to socket */
}

-- Connect (performs the full TLS 1.3 handshake)
let conn ← LeanTLS.TlsConnection.connect stream "example.com"

-- Send application data
conn.send data

-- Receive application data
match ← conn.recv with
| some data => /* process data */
| none      => /* connection closed */

-- Shutdown
conn.shutdown

/-- Abstract byte stream wrapping any transport. -/
structure IOStream where
  read  : Nat → IO ByteArray
  write : ByteArray → IO Unit

/-- TLS connection configuration. -/
structure TlsConfig where
  serverName     : String := ""
  skipCertVerify : Bool   := true

/-- High-level TLS connection handle. -/
structure TlsConnection

namespace TlsConnection
  def connect  (stream : IOStream) (hostname : String) (config : TlsConfig := {}) : IO TlsConnection
  def send     (conn : TlsConnection) (data : ByteArray) : IO Unit
  def recv     (conn : TlsConnection) (maxBytes : Nat := 16384) : IO (Option ByteArray)
  def shutdown (conn : TlsConnection) : IO Unit
end TlsConnection

lake build

All cryptographic primitives are tested against RFC/NIST official test vectors.

lake build tests && .lake/build/bin/tests

Test coverage:

lake build integration-test && .lake/build/bin/integration-test

Performs a full TLS 1.3 handshake with certificate verification enabled against mozilla.org and verifies the HTTP response.

• ECDSA (P-256) signature verification — Support ecdsa_secp256r1_sha256 (0x0403). Requires P-256 elliptic curve arithmetic implementation
• Certificate chain validation — Verify the trust chain from leaf through intermediate CAs to a root CA. Requires loading the system root CA store
• Certificate expiry checks — Parse ASN.1 UTCTime / GeneralizedTime and compare against current time
• CRL / OCSP — Certificate revocation checking
• AES-256-GCM — Support the TLS_AES_256_GCM_SHA384 cipher suite
• TLS 1.3 session resumption — PSK (Pre-Shared Key) based session resumption (0-RTT)
• Client certificates — mTLS (mutual TLS) support
• Formal verification — Leverage Lean's proof capabilities to formally verify correctness of cryptographic primitives

• RFC 8446 - TLS 1.3
• RFC 7748 - X25519
• RFC 5869 - HKDF
• RFC 2104 - HMAC
• FIPS 197 - AES
• NIST SP 800-38D - GCM
• RFC 8017 - PKCS #1 (RSA-PSS)
• RFC 6125 - Hostname verification
• RFC 8448 - TLS 1.3 test vectors

MIT