C*: Unifying Programming and Verification in C

Join the discussion

• Hacker News
• There already is a C* : https://en.wikipedia.org/wiki/C*
  by jensgk
• 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.

  by IsTom
• Names for C successor languages are pretty well exhausted by this point, so I sympathize, but I strongly associate the name C* with a decade-old rant about C compilers’ aggressive exploitation of undefined behavior: https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20... . (In calling it a rant I don’t mean that it’s altogether unpersuasive. Its style is just a bit spicier than I am used to seeing typeset in Computer Modern.)
  by gdwatson
• > We claim that C achieves real-time program verification, i.e., the user can carry out verification as they program the implementation code incrementally. It achieves this goal by orchestrating the symbolic-execution engine and the LCF-style proof kernel together, creating a proof-supporting runtime that runs proof-code blocks and symbolic execution of program segments in an interleaving manner

  That's why such thing is mostly useless. C is used in places where performance is important and nobody want to sacrifice performance for such proofing. Even more, if such proofing is too slow, it's better to use something like Fil-C.

  by Panzerschrek
• 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*.

  by Taikonerd
• 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...

  by gavinray
• The "C*" language website - https://cstarlang.org/en/intro.html

  See in particular, usage benefits with LLMs (last para of https://cstarlang.org/en/intro.html) and how to use it with LLMs (https://cstarlang.org/en/tutorial/cstar-mcp.html).

  Note that the paper/language are from 2025 and so pretty recent.

  by rramadass
• 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 toolset. There are certainly efforts and crates available in that direction, so hopefully others will bring it to where it needs to be. Lean is another one I have been playing with for some of the more overall logic proof of the system we are building.
  by eggy