C*: a proof-integrated C language unifying programming and verification
jedisct1 · x · 2026-09-09
An arXiv paper introduces C, a proof-integrated language design for C.
- C extends C with a symbolic execution engine and an LCF-style proof kernel, letting programmers embed proof-code blocks alongside implementation code with real-time, interactive proof-state updates.
- It targets the gap where conventional programmers rarely verify their own code due to disconnected programming/verification environments.
- Supports reusable libraries of logical definitions, theorems, and programmable proof automation.
- A prototype was evaluated on small C program benchmarks and a real-world case study: the attach function of pKVM's buddy allocator.
More from coding & agent
- Nex launches open source Nex-N2.5 agent models, Max hits 50.2 on AutomationBench near Claude Opus 5 — multimodalart · 2026-09-09
- Codex can generate tool-calling code on the fly — a new failure point for agent devs — srchvrs · 2026-09-09
- Paper: general coding agents beat purpose-built data agents by up to 37 points — RishiBommasani · 2026-09-09
- astra-chess: open-source Codex + skills setup for playing chess with GPT-6 Astra — MikePFrank · 2026-09-09
- Weaviate shows how to turn a messy creative archive into semantic search without renaming files — philipvollet · 2026-09-09
- Factory Worker 'Raises' a Local Gemma 31b AI in a Folder — She Gave Herself a Sense of Touch — D33lix · 2026-09-09