Lean 4 as a systems-programming and verified-interface language.

Seven repositories form one ecosystem: Bazel-native Lean build tooling, Protocol Buffers code generation, a pure-Lean gRPC runtime over HTTP/2, refinement-typed protobuf validation, checked PostgreSQL DDL/query code generation, a PostgreSQL client, TLS 1.3 over HACL* verified cryptographic primitives, and an integrated example service.

Start with lean-acme-widgets — the example service that integrates the ecosystem. The defining verified-interface pattern is implemented by protovalidate-lean: externally declared CEL constraints (buf.validate) compiled into ordinary Lean subtypes and dependent propositions, with proof-carrying values constructed at the decode/validation boundary — so handlers consume data whose validation and policy evidence is machine-checked.

Everything builds with Bazel, and the repositories expect side-by-side checkouts (they reference each other with Bzlmod local_path_override):

for r in rules_lean grpc-lean protovalidate-lean tls13-lean pg-lean lean-pgx lean-acme-widgets; do
  git clone "https://github.com/pb64-lean/$r"
done
cd lean-acme-widgets
bazel test //...

Prerequisites: Bazel 8.5 (every repo pins .bazelversion; bazelisk recommended) and Nix (the Lean toolchain is nix-built). The live end-to-end scripts additionally use Docker Compose, grpcurl, and openssl.

• Canonical build and test tool: Bazel via rules_lean. bazel test //... in each repository is the validation command.
• Canonical compiler: Lean 4.31.0-pre-24bef91, built by Nix from a pinned nixpkgs revision plus a lean4_upstream_std overlay (the pinned compiler provides the required Std.Async networking modules). Five repositories consume the overlay from grpc-lean/third_party/Lean-zh/protobuf/nixpkgs.{nix,json}; rules_lean carries its own copy of the same pin, and lean-pgx requests that matching toolchain through rules_lean.
• lean-toolchain files are editor/elan selectors only — no Bazel build reads them. Most repos name v4.27.0 for host editor tooling; grpc-lean names a local elan alias that tools/link-lean-nix-toolchain.sh links to the same nix-built 4.31-pre so the language server matches Bazel exactly.
• Lakefiles primarily provide IDE project models (they let lake serve resolve the module graph and sibling imports). Bazel remains the supported build and test path; lean-pgx can also build its handwritten library with Lake, but code generation and integration tests remain Bazel-only. rules_lean and protovalidate-lean have no lakefile at all.
• Compatibility: all modules use version 0.1.0 and resolve sibling dependencies through local_path_override. The supported configuration is the pinned repository set built together. Registry releases, version tags, and cross-version compatibility are outside the published compatibility contract.

Hermetic bazel test //... runs for every repository on self-hosted NixOS runners (push to main, weekly, and on demand), including the grpcurl interop suite for grpc-lean. lean-pgx exercises transient PostgreSQL 17/18 generation, cross-major compatibility, live generated APIs, and a standalone downstream Bzlmod consumer. Integration suites run on a docker-capable runner: the live PostgreSQL 17/18 matrix for pg-lean (quick subset on push, the full 26-combination matrix weekly) and the Acme end-to-end scenarios (plaintext, TLS, and in-process gRPC-over-TLS). A GitHub-hosted assurance scan runs on every push and pull request: it fails on sorry/ admit, inventories axiom/unsafe/@[extern]/partial def, handwritten C, and vendored trees, and reports the toolchain and dependency pins.

Repository	Hermetic	Integration	Assurance
lean-acme-widgets
protovalidate-lean		—
grpc-lean		(interop in CI)
lean-pgx		(PG17/18 + downstream in CI)
pg-lean
tls13-lean		—
rules_lean		—

The HACL* cryptographic primitives carry externally machine-verified correctness proofs and enter Lean through a small, explicit C shim with @[extern] bindings.

The Lean protocol code combines executable tests (known-answer vectors, live-server matrices, and end-to-end scenarios) with kernel-checked laws about the implementation itself, rather than a parallel specification model. Representative results:

• TLS: nonces never repeat within a traffic-secret epoch across a connection's emissions (resting on one named KDF-injectivity assumption, since HKDF is an opaque HACL* binding); the record framer conserves bytes and is independent of how the stream is fragmented; handshake codecs round-trip with unknown/GREASE values preserved; a parsed ClientHello re-encodes to its own bytes, and retry processing preserves that exact-byte identity; the key schedule structurally refines RFC 8446 §7.1; strict-DER exact-slice retention reaches the bytes certificate signatures are verified over.
• PostgreSQL: a pipelined client cannot misattribute a response — every user-visible success pops exactly the head operation, in submission order — plus Sync-recovery alignment, and codec round-trips including the lossless base-10000 numeric.
• Generated PostgreSQL APIs: declared DDL and literal SQL are replayed against PostgreSQL into canonical symbolic schema/query IR and typed Lean APIs. Generated validators construct proofs for the explicitly supported local constraint subset; attachment and prepared-query checks detect catalog and descriptor drift. An exact assurance target pins public theorem statements and the trust inventory, but does not prove arbitrary SQL, PostgreSQL behavior, or that a live database realizes the relational model.
• gRPC: RPC-shape agreement is structural rather than runtime-checked; a stream rejected at headers can never accept a body or reach a handler; flow-control credit is conserved; codec laws run up to HPACK Huffman decode∘encode.
• Generated code: every protovalidate-annotated message ships validate_sound / validate_complete theorems, and the example service binds its authorization propositions to an unfabricable authenticated principal.

What is not claimed: no refinement theorem against any RFC as a whole, no security proofs, no timing analysis, nothing about the C shims beyond their preconditions. Each repository's README states its own boundary, and lean_assurance_test targets audit the compiled environment on every build — axiom closures, sorry reachability, and @[extern] inventories pinned to the exact modules allowed to contain them. tls13-lean, pg-lean, and lean-pgx's audited Pgx module surface close over only propext, Classical.choice, and Quot.sound.