Skip to content

Home

Jump to bottom
Phillip Allen Lane edited this page Apr 16, 2026 · 3 revisions

What is Castor?

Castor is a tool that bridges the ROSE compiler framework with the Why3 verification framework. Currently, the only supported frontend is C++, but we are looking at more frontends in the future.

Castor in its current state is an in-development tool enabling formal verification of idiomatic C++. C++ can be written with verification conditions embedded in #pragma statements, and Castor will convert the program into a WhyML program which can be verified by the Why3 framework, including automated verification with SMT solvers.

There is currently limited but growing support for C++ features, and a custom verification language for writing verification conditions. These are outlined in this manual.

Table of Contents

  1. Implementation Decisions - Overviews certain implementation decisions made by Castor for C++ features that are left implementation-defined
  2. Supported C++ Features - Outlines the currently supported subset of C++
  3. The Verification Language - Outlines the grammar and basic usage of the verification language
  4. Verification Language Builtins - Outlines certain builtin functions and literals to the verification language to assist in expressing verification conditions
  5. What is Verified? - Explains what all Castor checks in addition to proving VCs

Release

This software manual is released as LLNL-SM-2018190.

This document was prepared as an account of work sponsored by an agency of the United States government. Neither the United States government nor Lawrence Livermore National Security, LLC, nor any of their employees makes any warranty, expressed or implied, or assumes any legal liability or responsibility for the accuracy, completeness, or usefulness of any information, apparatus, product, or process disclosed, or represents that its use would not infringe privately owned rights. Reference herein to any specific commercial product, process, or service by trade name, trademark, manufacturer, or otherwise does not necessarily constitute or imply its endorsement, recommendation, or favoring by the United States government or Lawrence Livermore National Security, LLC. The views and opinions of authors expressed herein do not necessarily state or reflect those of the United States government or Lawrence Livermore National Security, LLC, and shall not be used for advertising or product endorsement purposes.

This work performed under the auspices of the U.S. Department of Energy by Lawrence Livermore National Laboratory under Contract DE-AC52-07NA27344.

This document is released as LLNL-SM-2018190.

Clone this wiki locally