[0xbadcafebee]

I forget sometimes that the papers and talks issued by teams at most companies are for PR and resume-padding. They hype the findings that justify that team's budget, and bury any negatives.

The other funny thing I noticed is the formal verification just means the program implements the standard - it doesn't mean the standard doesn't have security holes! And sometimes the security holes are implementation-specific, like timing attacks, which can require weird low-level tricks to solve.

[edelbitter]

>bury any negatives

I was looking for the x86-specific rant, and did not find it. You'd think that team would have had something to say about architecture complexity.

[transpute]

Nvidia’s GPU root of trust, where they are using SPARK, is based on RISC-V, they have a talk about that choice, https://news.ycombinator.com/item?id=43045952