lean-grpc
Lean 4 gRPC stack — HPACK, HTTP/2, and gRPC framing on Std.Async.TCP. Version 1.1.0. Apache-2.0.
Open source
Formal work, published
Riley Betts publishes formal methods work. The Lean protocol stacks are patterns you can read, and can commission. Open source is the evidence. You reach them through the Lean-proved software engagement.
lean-tee
lean-tee (trusted execution environment). The implementation is a zkVM (zero knowledge virtual machine): measured execution, hashed receipts, and lean-grpc APIs. Not a confidentiality enclave. Apache-2.0.
nuropb-rmq
An async Python AMQP 0-9-1 client, with no pika, and JSON-RPC mesh patterns. SMT specifications check the protocol rules. Lean proves properties of that AMQP model. The Python client matches the model. It is not generated from the proof. Apache-2.0.