ACSL (ANSI/ISO C Specification Language)

Overview

ACSL (ANSI/ISO C Specification Language) is a formal specification language for the C programming language. It is based on an axiomatic semantics for C in the style of Hoare logic, and is the primary language used to annotate C source code for the Frama-C framework — an extensible set of interoperable program analyzers for C.

Semantics and Design Rationale

ACSL provides a Hoare-logic / weakest-precondition foundation for expressing properties of C programs (preconditions, postconditions, loop invariants, predicates over memory, etc.). Most of the analyzers bundled in Frama-C consume ACSL annotations as the formal contract format that drives deductive reasoning about C code.

Integration with Frama-C

Frama-C processes ACSL-annotated C code by leveraging the Why platform, an implementation of Dijkstra's calculus of weakest preconditions. The pipeline is:

ACSL-annotated C is compiled into Why's intermediate verification language.
A Verification Condition (VC) generator emits proof obligations from the annotated program.
Those obligations are dispatched to automatic provers (e.g., Alt-Ergo, SMT solvers) and/or to interactive provers such as Coq.

Within Frama-C, the WP plugin is the main deductive-verification backend that consumes ACSL annotations and produces VCs for a range of SMT solvers. The RTE plugin complements this by automatically generating ACSL annotations that capture run-time error behaviors, providing a baseline of annotations for code that is otherwise unannotated.

Applications

Avionics and DO-178C compliance

ACSL combined with Frama-C's WP plugin (and Alt-Ergo as the back-end prover) has been used experimentally to formalize and partially verify low-level software requirements extracted from a real DO-178C-compliant avionics project, supporting the formal-methods supplement DO-333. The study highlighted both the fit-for-purpose criteria of the approach in an SME context and issues that typically arise when applying deductive verification to embedded real-time C code.

Certified instruction-set simulation

ACSL/Frama-C has been used in research on verified faithful simulation of instruction-set architectures (e.g., ARM), where the goal is to prove that a C-coded simulator produces results identical to a formal executable model of the architecture. Such efforts require substantial ACSL annotation libraries, custom proof tactics (e.g., new inversion tactics in Coq), and careful handling of the C features accepted by the toolchain.

Automated annotation generation

Because hand-writing ACSL is expensive, recent empirical work has compared strategies for automated ACSL annotation generation on real C programs (a filtered subset of the CASP benchmark), evaluating:

a rule-based Python script,
Frama-C's RTE plugin,
three large language models (DeepSeek-V3.2, GPT-5.2, OLMo 3.1 32B Instruct) in a one-shot setting.

Annotations produced by each strategy were assessed through Frama-C's WP plugin with multiple SMT solvers, comparing proof success rates, solver timeouts, and internal processing time. The reported finding is that rule-based approaches are more reliable for achieving verification success, while LLM-based methods show more variable performance, suggesting LLMs are best seen as complementary tools rather than drop-in replacements for rule-based annotation generation.

Relation to Operational-Semantics Approaches

ACSL is fundamentally an axiomatic-semantics approach. By contrast, projects such as CompCert define an operational semantics for a (deliberately restricted) subset of C, formalized in Coq. Work on certifying C-level ARM instruction-set simulators has had to choose between the two:

ACSL/Frama-C offers rich abstraction mechanisms, good ecosystem, and a large body of C-language support, but is tied to the C semantics understood by Frama-C and to its provers.
Operational-semantics approaches in Coq (as in CompCert) give a state-transition view of C execution that is closer to compiler-correctness proofs and to a certified C compiler, at the cost of accepting only a smaller subset of C.

Similar trade-offs appear in large C-implementation verification efforts such as seL4, which also derives proof obligations from C code but treats the compiler and architecture as correct rather than modeling their semantics directly.