Jean-Karim Zinzindohoué

AFAIK TLSExtension is not verified so far. I will look a bit into parsing/serializing in the coming days to verify parts of it. Please let me know if you plan...

What are the Low\* libraries ? Are FStar.HyperStack, FStar.HST and FStar.Buffer part of it ?

I think that the machine integers are independent from Low*. They define native OCaml integers for instance.

So the standard library will no longer be unified under the `FStar` name ?