4 ms·
i've been working on and off (mostly off) on https://robigalia.org/ https://robigalia.org/ for five years now, and interned with the sel4 verification team. fee
by cmrx64 6y ago
i've been working on and off (mostly off) on https://robigalia.org/ https://robigalia.org/ for five years now, and interned with the sel4 verification team. feel free to swing by freenode#robigalia if you you want to chat sel4 or trustworthy software, there's a small group collected over the years that would love to answer your questions :)
- mlinksva 6y agoThanks for posting. ~yearly I look at your site (idly, not likely to have anything to contribute) because Robigalia sounded very interesting when first discussed here at https://news.ycombinator.com/item?id=10848890 https://news.ycombinator.com/item?id=10848890
- cmrx64 6y agoty for the kind words! i'm hoping 2021 will bring a working demo of some basic goals :) the rust ecosystem has moved a long way since 2015, async/await finally being everywhere is a gamechanger because almost everything is async/await for us!
- kaba0 6y agoWhat’s your opinion on the scalability of formal methods? Isn’t it still the case that basically formal verification is impossible to do for larger code bases (like at least 10-100x that of sel4 in lines of code) and even sel4 took many many years and experts?
- cmrx64 6y agocurrent tools, verifying C code like seL4? never going to happen. but i'm hopeful about new techniques, things like the work Amal Ahmed http://www.ccs.neu.edu/home/amal/ http://www.ccs.neu.edu/home/amal/ is doing. you don't need to formally verify the entire codebase for basic properties like "can compose with the sel4 proofs" if your runtime/compiler/language/OS is all participating. right now you have to fight against the fact that none of the software of interest is well-understood mechanically by other software.