The RISC-V architecture is a potential candidate for later verification. Would you be interested in trying to keep your C port in the subset of the C language our verification tools can handle? It may be more work for your project, but it will give you the real seL4 experience ;-)
If yes, I can give you some tools and instructions on how to use them for checking the subset. There’s a lightweight syntax-only checker, and there’s a longer-running check that actually reads the code into the theorem prover.
That will be great. Actually I was thinking of formally verifying the port, but since I don't have experience with formal verification in general, I wouldn't know how much time/effort would this take, given that I heard you did the verification in 20 years and more than 100K of code :)
Cool, give me a few days, and I’ll put some docs together (new prover version is just coming out today, so will need to update the infrastructure first). Updating the whole verification is probably too much for the timeframe of the project, but updating the formal specs and Haskell prototype might be useful and even helpful for your project. If you’re interesting in that, let me know. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.