1.0.0

[MattCCC]

C++L 1.0.0 — V1

Provable C++, without replacing C++. State what must be true, prove it, remove the proof layer, and ship ordinary native C++.

Warning

1.0.0 is stable but not production-ready. "Stable" means the language, grammar and kernel calculus are frozen. Until the maintainer has finished reviewing the kernel and testing the proofs more, treat C++L as potentially unsafe for production applications.

Highlights

• C++ first. C++17, C++20 and C++23 code keeps its meaning. Code outside verified functions goes to Clang unchanged. If you use a C++L word as a C++ name, it keeps its C++ meaning and the compiler warns you.
• Kernel-checked proofs. Every PROVEN claim comes from the proof kernel accepting exactly that goal. The kernel has 15 rules and adds no axioms. A Coq model of how the kernel checks proofs is proven sound and consistent, and the C++ kernel is tested against that model.
• Contracts. expects, ensures, decreases and loop invariants on functions, member functions and function templates. Contracts hold inside one translation unit and across units through checked verification interfaces.
• Laws, equality, induction and termination. law declarations, propositional Eq<T> with rewrite, induction over unsigned machine integers, and termination measures.
• Refinement types. type R = T where (...). A value gets a refinement type either through a static proof or through an explicit validate<R>(e), and every report names the validation site.
• A verified C++ subset (RFC 0022). 96 constructs are verified, each with a refused counterpart that shows the model really checks it. 55 constructs are refused, each with its own diagnostic. The verified subset covers:
  • machine arithmetic, including overflow, conversion and division
  • references and aliasing
  • models of std::vector, std::array and std::span
  • struct values
  • short-circuit &&, || and ?:
  • if, switch and range-based for
  • enumerations, constant globals and default arguments
• Proof erasure. Proof-only text is blanked out and checked. The assembly of the erased program matches the assembly of a hand-erased version at -O0 and -O2.
• Trust reporting. Text and JSON reports, and the editor, list everything each claim depends on: trusted laws, library models, unsafe code, imported contracts and runtime validations.
• Tooling.
  • cppl, the compiler, which accepts clang++'s command line
  • cppl-format, the formatter
  • cppl-lsp, the language server
  • editor support for VS Code, JetBrains IDEs, Visual Studio and Neovim

Release metadata

Kernel	cppl-kernel-0.9.0
Formal core	cppl-core-0.9.0
Verification semantics	cppl-verification-9
Verification-interface format	v3
C++ modes	c++17, c++20, c++23
Platform	Linux x86_64 (Ubuntu 24.04), LLVM/Clang 22.1.8, libstdc++ from GCC 13.3
ABI guarantee	none beyond Clang's own

Not supported in V1

Everything below is refused with a diagnostic, so none of it can be counted as verified by accident:

• existential quantification and proof let
• the proof-only @ domains
• kernel type families
• shifts and bitwise operators
• concurrency, and pointers beyond the modeled references and views
• base classes, unions and user-provided copy operations in verified structs
• library types other than the modeled containers, such as std::optional and std::string_view
• reading a container element in a contract or invariant, except an array element at a constant index
• switch init-statements and if consteval

Trust

A PROVEN claim holds relative to the trusted components listed in its report: the kernel, the C++-to-proof translation (which is not itself verified), the toolchain, and any trusted laws, library models, unsafe code, imported contracts and runtime validations it depends on. See TRUST.md.

Compatibility

Verification interfaces written by earlier builds are refused because the verification semantics changed.

---

Docs: INSTALL · STATUS · SPEC · CHANGELOG

---

This discussion was created from the release 1.0.0.