c_verif_seplogic_lean4

This project is an experimental project using separation logic for doing C program formal verification in Lean 4. This project is co-developed with Codex and Claude Code.

This is an experimental project that is WIP.

The core C operational semantics of the formal verification framework is based on a Lean 4 port of the CompCert frontend: https://github.com/rdevshp/c_operational_semantics_lean4.

The source code might contain LLM generated comments that have not been properly manually reviewed.

Work remains to be done to perform a proper manual review on the various abstractions and definitions used in this project.

Build every root Lake target and standalone proof fixture, all example workspaces, and all Rust importer targets with:

tools/build_all.sh

Clean the root Lake workspace, every standalone example workspace, and the Rust importer build artifacts with:

tools/clean_all.sh

Standalone C verification examples live under examples/. Elaborate all example artifacts with:

tools/elaborate_examples.sh

Use tools/elaborate_examples.sh --check to check that the committed Lean modules still exactly match their C inputs.

Run tests with:

lake exe parser_tests
lake exe parser_generator_tests
lake exe parser_vy_importer_tests
lake exe parser_vy_full_grammar_tests
lake exe parser_vy_lr_validation
lake exe semantics_tests
lake exe csyntax_notation_tests
lake exe elab_tests

Run the complete repository verification with:

tools/verify_all.sh

Use tools/verify_all.sh --lean-only when Rust tooling is checked separately.

Generate a Lean module containing the Cabs AST for a C translation unit with:

lake exe c_parse_export --namespace GeneratedCParse.Example input.c Generated/Example.lean

Generate a Lean module containing the elaborated CProgram for a C translation unit with:

lake exe c_elab_export --namespace GeneratedCProgram.Example --main main input.c Generated/Example.lean

The generated elaboration file records sourcePath, source, mainName, symbols, typedefs, functionNames, and program.

Lean code can quote complete C expression and statement trees with the C-shaped notation exported by CSem.Cfrontend.Csyntax. For example, cexpr%[(get(x)@typeInt32s + i32(1))@typeInt32s] and cstmt%[if (i32(1)) { return i32(42); } else { return i32(0); }] expand to Expr and Statement; cexprs%[...] constructs argument lists. The C elaboration exporter uses these forms in generated modules.

Separation-logic assertions have a notation under open scoped SLProp: use P ∗ Q for binary separating conjunction, ⌜p⌝ for a pure fact, and ∃ₛ x, P x for an assertion existential. For larger spatial contexts, sep%[P, Q, R] expands to the right-associated P ∗ Q ∗ R; sep%[] is SLProp.emp.

The parser test runner reads a case manifest from Tests/parser_cases.txt by default. Each manifest entry points at a .c source file under Tests/parser_cases/. Pass another manifest path as the first argument to use a different fixture.

Regenerate or inspect the imported Parser.vy grammar with the Rust importer:

tools/parser_vy_importer path/to/Parser.vy --emit summary

The wrapper dispatches to the Cargo project in tools/rust.

The Lean toolchain is pinned in lean-toolchain.

License:

This project is distributed under the GNU Lesser General Public License, version 2.1 or, at your option, any later version. Portions are derived from the CompCert verified compiler 3.17, whose relevant cfrontend/, cparser/, common/, and lib/ files are available under LGPL-2.1-or-later. See LICENSE and NOTICE.