Sorry to hear you had issues with my comment system. Comments are invisible until I manually approve them, but I'm not seeing anything new in the database right now. Did you get any sort of error code? The system should let you know if e.g., the answer to the captcha was wrong.
I do mention SPARK at the end of the article. I'm not familiar with Frama-C so I'll check that and your blog posts out. Thanks for sharing!
Sorry I missed the mention of SPARK. TLA+, although I haven't fiddled with it as much, is more similar to Alloy than anything else. SPARK actually works on Ada code.
I do mention SPARK at the end of the article. I'm not familiar with Frama-C so I'll check that and your blog posts out. Thanks for sharing!