News for hackers. Stuff that matters.

A comment on Memory Safe Languages in Android 13. Parent comment

Re:Memory Safe Languages in Android 13 by KMag on Friday December 02, 2022 @02:34AM (#33827876)
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.
[ Parent | on HN ]

There are no comments on this comment yet.