C*: A New Language That Lets C Programmers Verify Their Own Code in Real Time
C*: Unifying Programming and Verification in C
Formal verification of systems software is crucial but rarely done by the programmers who write the code, due to the disconnect between programming and verification environments. Researchers introduce C*, a proof-integrated extension of C that embeds verification capabilities directly into the language. With C*, developers can write proof-code blocks alongside implementation code, enabling real-time, interactive verification through a symbolic execution engine and an LCF-style proof kernel. C* unifies programming and proof development by using C as the common language, and its expressive proof support allows building reusable libraries. Evaluated on a benchmark of small C programs and a real-world case study (pKVM's buddy allocator attach function), C* demonstrates broad coverage of C idioms and effective handling of complex reasoning.
C* unifies implementation and proof code development by using C as the common language.
- eggy
I've been on this horse for a while now. I've settled on learning Ada/SPARK. Ada 2022 will start feeding a new SPARK 2014 update. Yes, they are both verbose, if you don't like that sort of thing, and don't like Pascal-like syntax. Believe me, I like APL/J/k/uiua/BQN and Forth and ASM. I am usually syntax agnostic as long as the PL and the ecosystem (more important than most think), meet your needs. I tried Rust back in 2018, and then again in 2023, but found it very complex and Ok, not a fan of the syntax. I would have preferred more ML or Haskell-like syntax. Zig seemed nice, but different use case, and too new. After all, Ada/SPARK have been on huge, high-assurance, high-safety applications for decades. Rust is getting some of their love, and vice versa. AdaCore had created a verified Rust compiler, but with a real world product (Blacktail hoist) in the works, we need a toolset and guarantees and ease of auditing and acceptance to achieve high safety and standards certifications. Think aerospace, defense, railway, and automotive. I started programming in 1977, so there's always a place in my heart for ASM/C. I played with F#, F*, and LOW from MS, and they are good, but they and Rust simply don't have the real world legacy of Ada/SPARK. I have been using Shen to write some formally verified models of less safety-critical areas of our software and I find it refreshing, however, my day job is to stay focused on Ada/SPARK until Rust matures more with a formally verifed proven t […]
- IsTom
I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with ergonomics, but it leaves a lot of space for specification bugs.
And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.
- slowcache
I think formal verification is a super interesting field, but this is a non-starter for me because I do not have a backwards E on my keyboard
- gavinray
I really think that verification aware languages are going to become a necessity
Wrote a bit about this recently
https://gavinray97.github.io/blog/design-by-contract-and-eff...
- Taikonerd
The authors cite this, but just to mention it: this sounds like F*, another proof-oriented language. (https://fstar-lang.org/)
F* is in the ML family of languages, so it looks pretty different from C*.