logoalt Hacker News

pixl97yesterday at 8:41 PM1 replyview on HN

Are people willing to pay the cost of this formal verification. Especially when it needs done at the hardware, firmware, and kernel levels.


Replies

amlutoyesterday at 9:37 PM

seL4 is willing to pay, but they're mostly targetting a different use case: running programs targeting seL4, which isn’t what typical agentic workflows want. You can, however, run Linux on seL4, and maybe agent sandboxes should start using it. And ARM is, at least sometimes, interested in helping out with security and formal verification research.

Also, the cost of verification is trending pretty sharply downwards.