4 ms·

Now that is interesting. I didn't know that and will have to look further to understand what it means. Wireguard seems to be written almost entirely in C, is t

by harry8 4y ago

Now that is interesting. I didn't know that and will have to look further to understand what it means. Wireguard seems to be written almost entirely in C, is that right?

KMag 4y ago
The symbolic proofs of the protocol are independent of the implementation. The portions of the implementation that are formally verified are written in F* and Coq, and emitted as machine-generated C.