A few people have shown interest in SPARKTLS - a TLS 1.2/1.3 library I’ve been working on for quite a while. It started as a science project, but the advent of smarter and smarter LLMs has rapidly accelerated my progress over the past few months to the point where it’s probably ready for others to start experimenting with or at least looking at and throwing spears 
With that: a big caveat - this is HEAVILY LLM-written. I won’t say “vibe-coded” because it has been in the works for years, and the last few months have been filled with lots of back-and-forth with various AI agents and lots of manual effort on my part. But if you are not comfortable with AI code, this is not the library for you . There is still a lot of sloppy comments, inconsistencies etc. scattered throughout the codebase, pending my cleanup and a more thorough manual review before alpha release.
The core library relies on RecordFlux (and uses a slightly modified version of their example TLS specifications) for the TLS parsing/building code, Rod Chapman’s SPARKNaCl project, and then my SPARKx509, SPARKTLSCrypto repos. The examples use SPARKEntropy as a userspace random number generator using the jitterentropy technique and the SPARK library libkeccak.
I don’t have a handy Alire crate published yet (I will when I’m ready to call it alpha release) but you can pin a relative path in your application and use it that way.
It relies strictly on BIO-style input/output buffers and the API looks a little different than OpenSSL. This was done so the core library can remain 100% SPARK, and the socket and file I/O (for trust stores, etc.) can be kept outside using callbacks, and can be used with modern I/O techniques like io_uring. (An asynchronous web server example w/ epoll is provided).
DO NOT trust this with production data. I have gotten 100% proof discharge on SPARKEntropy/SPARKx509/SPARKTLSCrypto and the core library itself, and have made reasonable attempts to ensure constant-time crypto (testing with ctgrind and dudect) but that is not a substitute for experienced cryptanalysis by experts.
I have used several test suites against it including the BoringSSL BoGo suite, TLSfuzzer, google/x509test and x509-limbo, and these demonstrate mostly-compliant behavior.
Full proof takes about 3 hours on my Ryzen 9950X3D with 128G of RAM, you will need the Colibri library installed as well to discharge some of the RecordFlux proofs.
I hesitate to make performance claims because benchmarks can be finicky to get an apples-to-apples comparison, but my limited testing indicates performance is competitive with OpenSSL for handshakes and certain cipher suites. RSA signature verification is notably slower (improvements forthcoming). There are non-SPARK ASM routines to provide hardware acceleration if available, for some of the crypto algorithms.
There’s a CLI tool comparable to the openssl tool - sparktls_cli - which is not as feature-filled as openssl, but was meant to be a more user-friendly way of doing some of the things that openssl does and experiment with a different style of CLI flags.
Again - this is all pre-alpha, still in need of a lot of cleanup and review, and NOT suitable for production use. Hopefully some of you may find it interesting or useful, and I think it’s a good showcase for the type of work that LLMs are able to do with Ada/SPARK.
I’ll post again when I’m ready to call this an “alpha release” but happy to chat about the project here in the meantime.