1. 2

A TLS library implemented with modern techniques to improve security. These include a memory-safe language, pure functions where possible, type-checking protocol steps, and a DSL for easier parsing. Result is library and runtime with 73-84% of bulk performance of unsafe OpenSSL with 25x less code in trusted, computing base.

    1. 1

      Github is here:

      https://github.com/mirleft/ocaml-tls

      Those interested in an imperative implementation can still benefit. The method would be to use Ocaml as a safer, reference implementation for a derivation into SPARK Ada, a statically-checkable subset of C, or Rust. The verification tools of SPARK or C are run on the resulting code.