I was in that comment section bringing up RV-Match. The difference is that RV-Match is a bunch of static-analysis functionality built on a comprehensive semantics for C. KRust is a tiny subset of Rust with RV-Match-style analysis. I did bookmark it in case it could be useful for someone trying to build that.
"where they are very interested in formal proofs"
The only thing I mentioned that would be doing a formal proof was the lightweight stuff like Frama-C and SPARK Ada that don't require proof so much as annotation (eg like borrow checker) that run through automated provers. The rest was all push-button or no-proof-needed tools that say something has no errors, specific errors, or a mix of them and false positives. RV-Match and Astree Analyzer will straight-up tell you that specific errors don't exist with low, false positives. The test generators that work on structure of your code get deep into lots of errors from different combinations of inputs and control flow. None of these require proof. People building these usually test them on FOSS projects, sometimes the same ones, often finding new errors in them.
"In terms of deadlocks, I’m not aware of anything here. "
Good to know. That be the focus area for now since you said livelocks are a good situation. I'll still keep an eye on the side for anything checking that.
"they might have some interesting options and a few of the people over there are very capable in answering these questions."
I was in that comment section bringing up RV-Match. The difference is that RV-Match is a bunch of static-analysis functionality built on a comprehensive semantics for C. KRust is a tiny subset of Rust with RV-Match-style analysis. I did bookmark it in case it could be useful for someone trying to build that.
"where they are very interested in formal proofs"
The only thing I mentioned that would be doing a formal proof was the lightweight stuff like Frama-C and SPARK Ada that don't require proof so much as annotation (eg like borrow checker) that run through automated provers. The rest was all push-button or no-proof-needed tools that say something has no errors, specific errors, or a mix of them and false positives. RV-Match and Astree Analyzer will straight-up tell you that specific errors don't exist with low, false positives. The test generators that work on structure of your code get deep into lots of errors from different combinations of inputs and control flow. None of these require proof. People building these usually test them on FOSS projects, sometimes the same ones, often finding new errors in them.
"In terms of deadlocks, I’m not aware of anything here. "
Good to know. That be the focus area for now since you said livelocks are a good situation. I'll still keep an eye on the side for anything checking that.
"they might have some interesting options and a few of the people over there are very capable in answering these questions."
Thank ya very much. I'll hit them up, too.