# SPARKTLS Updates
**URL:** https://forum.ada-lang.io/t/sparktls-updates/4730
**Category:** General
**Tags:** spark
**Created:** [September 9, 2026, 11:20pm UTC](https://forum.ada-lang.io/t/sparktls-updates/4730 "2026-09-09T23:20:44Z")
**Posts on this page:** 9
**Page:** 1
### Author:  [@docandrew](https://forum.ada-lang.io/u/docandrew)
#### Post date: [September 9, 2026, 11:20pm UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/1 "2026-09-09T23:20:44Z")
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 🙂
> **[GitHub - docandrew/SPARKTLS: TLS 1.3 Implementation in SPARK](https://github.com/docandrew/SPARKTLS)**
>
> TLS 1.3 Implementation in SPARK
> **[GitHub - docandrew/SPARKTLSCrypto: Crypto support for the SPARKTLS project](https://github.com/docandrew/SPARKTLSCrypto)**
>
> Crypto support for the SPARKTLS project
> **[GitHub - docandrew/SPARKx509: Verified library for X.509 certificates](https://github.com/docandrew/SPARKx509)**
>
> Verified library for X.509 certificates
> **[GitHub - docandrew/SPARKEntropy: SPARK Implementation of the Jitter RNG](https://github.com/docandrew/SPARKEntropy)**
>
> SPARK Implementation of the Jitter RNG
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.
> **[GitHub - damaki/libkeccak: SHA-3 and other Keccak related algorithms in...](https://github.com/damaki/libkeccak)**
>
> SHA-3 and other Keccak related algorithms in SPARK/Ada.
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.
---
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [September 9, 2026, 11:38pm UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/2 "2026-09-09T23:38:00Z")
this actually seems really interesting, thanks for sharing
---
### Author:  [@ksson](https://forum.ada-lang.io/u/ksson)
#### Post date: [September 10, 2026, 12:39am UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/3 "2026-09-10T00:39:51Z")
This is awesome. I will definitely look into this when I need TLS for some of my hobby projects. Don’t hesitate to throw bug reports at [GitHub - AdaCore/spark2014: SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications. · GitHub](http://github.com/AdaCore/spark2014), or give some user feedback here. Unfortunately the FSF version is more or less a “drop” and we don’t have a process in place to fix an existing release, but we can fix bugs in future versions.
---
### Author:  [@docandrew](https://forum.ada-lang.io/u/docandrew)
#### Post date: [September 10, 2026, 12:51am UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/4 "2026-09-10T00:51:30Z")
Thanks! I have run into a couple of gnatprove crashes that I was able to work around but will try and do a better job with bug reports when I do.
---
### Author:  [@kevlar700](https://forum.ada-lang.io/u/kevlar700)
#### Post date: [September 10, 2026, 11:52am UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/5 "2026-09-10T11:52:44Z")
> [@docandrew](#):
>
> RSA signature verification is notably slower (improvements forthcoming).
Sounds like it’s in the works but does anyone use RSA these days?
---
### Author:  [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)
#### Post date: [September 10, 2026, 12:17pm UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/6 "2026-09-10T12:17:48Z")
> [@kevlar700](#):
>
> Sounds like it’s in the works but does anyone use RSA these days?
For automation systems we did not use it (nor TLS). For encryption a symmetric ChaCha20 was used, AEAD was for signing (RFC 8439).
---
### Author:  [@docandrew](https://forum.ada-lang.io/u/docandrew)
#### Post date: [September 11, 2026, 2:12am UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/7 "2026-09-11T02:12:53Z")
Still pretty prevalent in government work. SPARKTLS can do signature verification w/ it but does not implement RSA keygen for use in new keypairs.
---
### Author:  [@mgrojo](https://forum.ada-lang.io/u/mgrojo)
#### Post date: [September 11, 2026, 7:23pm UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/8 "2026-09-11T19:23:24Z")
Does it support DTLS? I used WolfSSL in [CoAP-SPARK](https://github.com/mgrojo/coap_spark/blob/2fa345b8c70d621287b932aee7ea39b3520a5adf/src/coap_spark-channel.adb) and I’m interested in knowing if I could provide an alternate communication layer, also in SPARK.
---
### Author:  [@docandrew](https://forum.ada-lang.io/u/docandrew)
#### Post date: [September 11, 2026, 8:54pm UTC](https://forum.ada-lang.io/t/sparktls-updates/4730/9 "2026-09-11T20:54:11Z")
It does not support DTLS yet - TBH I wasn’t sure whether it was worth supporting or not, but the fact that you use it is a helpful data point!
I don’t think it would be a huge lift to add, since SPARKTLS itself is already transport-agnostic, but DTLS does have some minor differences that I’d need to address.