Hi all (Mike, Tom, Baris, Gilbert, Haoran), After submitting the DARPA proposal, Tom suggested we start thinking and doing what we would either want to have done by the time funds arrive or what we want to have done for an NSF large in 10 months or so. Haoran has already started looking at this problem, so would be great to concentrate on some useful starting examples, and keep posted on any progress. I suggested some libraries I'm particularly interested in: - TPM2, the reference implementation for the trusted platform module specification. - OpenThread or LwIP -- both network stacks used as "userspace" libraries - LVGL GUI library - BoringSSL/aws-lc -- we have work verifying the safety of the assembly against a Rust function parameter, the aws-lc people _want_ to have a version that is entirely Rust and it's likely relatively straightforward to port (e.g., there mostly aren't any complex data structures or anything. Three of the four have pretty robust test suites. Tom helpfully pointed out that some of these are likely too high a bar to start with, and that we really want to start with things that are fairly simple and almost certainly do not have bugs in them. -Amit