Axiomatic Reasoning for LLMs

Implementation Plan on C

1. Overview

This document provides a technical implementation plan for applying a specification-driven, AI-assisted development methodology to the C programming language. The methodology is built on four core principles:

C lacks object-oriented and template features, but function pointers, opaque pointers, static analyzers, formal verification frameworks, and code generators make the methodology practically realizable.

2. Structural Specification in C

Specification Type Representation Tooling Use Case
Data structures JSON Schema libjsonschema, zcbor Generate C structs + serializers
API contracts OpenAPI 3.0+ OpenAPI Generator (C) Generate libcurl‑based clients
Behavioral constraints ACSL (ANSI/ISO C Specification Language) Frama-C Formal verification of safety‑critical code

All specifications are machine‑readable and stored under version control. They serve as the single source of truth.

3. Generative Conformance Pipeline

Specification (JSON/OpenAPI/ACSL)
    │
    ▼ (code generation tool)
Generated C code (tissue layer)
    │
    ▼ (compiler + static analysis)
Validation gates (type safety, memory safety, architectural rules)
    │
    ▼ (pass/fail)
Commit / Reject

Recommended generators:

4. Skeleton‑Tissue Architecture

Directory Layout

project/
├── skeleton/          # Hand‑written, immutable (human only)
│   ├── core.h
│   └── processor.h
├── specification/     # Machine‑readable specs (JSON/OpenAPI/ACSL)
├── tissue/            # AI‑generated code (gitignored, regenerated)
├── generated/         # Tool‑generated code (gitignored)
└── tests/             # Test suite

Pattern: Template Method with Function Pointers

Skeleton (immutable)

typedef struct {
    void (*init)(void* ctx);
    void (*process)(void* ctx, const Input* in, Output* out);
    void (*cleanup)(void* ctx);
} VTable;

typedef struct {
    VTable vtable;
    void* ctx;
} Processor;

void processor_execute(Processor* p, const Input* in, Output* out) {
    p->vtable.init(p->ctx);
    p->vtable.process(p->ctx, in, out);
    p->vtable.cleanup(p->ctx);
}

Tissue (generated from specification)

static void my_init(void* ctx) { /* generated */ }
static void my_process(void* ctx, const Input* in, Output* out) { /* generated */ }
static void my_cleanup(void* ctx) { /* generated */ }

VTable my_vtable = { my_init, my_process, my_cleanup };

The skeleton owns the execution flow, so generated tissue cannot bypass architectural constraints.

5. Validation Gates

Level Tool Checks
Compile GCC/Clang Function signatures, type consistency
Static analysis PC‑lint Plus / Clang Static Analyzer MISRA/CERT, memory safety, null pointers
Unit tests Unity / Ceedling Functional correctness
Architecture Custom script + nm Dependency direction (no tissue → skeleton reverse deps)
Formal verification (optional) Frama‑C + ACSL Mathematical correctness (safety‑critical systems)

CI integration (GitHub Actions example):

- name: Generate Code
  run: cmake --build build --target generate
- name: Static Analysis
  run: pc-lint-plus lint-config.lnt tissue/*.c
- name: Verify No Uncommitted Generated Code
  run: git diff --exit-code -- generated/ tissue/

6. Recursive Refinement and Fixed Premises

Each development phase ends with a fixed premise – a Git tag (phase-N-complete) plus the current specification files. Subsequent phases treat this premise as immutable.

Workflow:

  1. Modify structural specification (JSON/OpenAPI/ACSL).
  2. Run build – code regeneration triggers automatically (CMake add_custom_command with DEPENDS).
  3. Validation gates run; failure rejects the change.
  4. On success, commit new specification and generated code, tag as next phase.

CMake integration:

add_custom_command(
    OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/generated/config.c
    COMMAND jsonschema2c specification/config.json -o generated/
    DEPENDS specification/config.json
    COMMENT "Regenerating C code from JSON Schema"
)

7. LLM Integration for Tissue Generation

When using LLMs (e.g., VeCoGen, NL2ACSL) to generate tissue code from specifications:

Prerequisites (from rsyslog 200k LOC experience):

Recommended stack:

8. Implementation Roadmap

Phase Duration Key Tasks Success Criteria
0 – Infrastructure 1‑2 w Setup CMake, static analyzer, Git workflow CI runs static analysis with zero warnings
1 – Specification 2‑3 w Define JSON Schema / OpenAPI; build codegen pipeline Generated code compiles without errors
2 – Skeleton‑Tissue 2‑3 w Implement function‑pointer patterns; enforce directory separation CI detects skeleton modifications
3 – Validation 1‑2 w Integrate static analysis + architecture tests Merges only after all gates pass
4 – LLM Integration 2‑3 w Add VeCoGen/NL2ACSL; write AGENTS.md Spec‑to‑code lead time <15 min
5 – Legacy Migration ongoing Strangler Fig pattern – replace modules incrementally Each module independently migratable

9. Expected Efficiency Gains (Based on Empirical Studies)

Project Type Estimated Effort Reduction
New greenfield project 40‑60%
Incremental adoption on legacy code 20‑40%
Interface‑heavy development (libraries, APIs) 50‑70%
Algorithm‑heavy development 15‑30%

These estimates derive from model‑driven development case studies (Wärtsilä, ATB Technologies) and LLM‑assisted development research (ICSE 2026, Peng et al.).

10. Constraints and Mitigations

Constraint Mitigation
Function pointer type safety Static analysis (PC‑lint Plus) enforces signature matching
ABI stability Opaque pointers + versioned structs + accessor functions
Memory safety (LLM‑generated code) Static analysis + Frama‑C formal verification
Specification writing cost NL2ACSL converts natural language to ACSL (74% success)
Team learning curve Start with pilot module (4 person‑days), document patterns

11. Minimal Pilot Implementation

Scope: Configuration module – JSON Schema → C structs + JSON parser.

Stack: libjsonschema, CMake, PC‑lint Plus, Git, GitHub Actions.

Effort: ~4 person‑days (env setup 1d, schema 0.5d, CMake 0.5d, skeleton 1d, verification 0.5d, testing 0.5d).

Success:

12. Conclusion

The C programming language, despite lacking modern abstractions, can fully support a specification‑driven, AI‑assisted development methodology using existing tools: JSON Schema/OpenAPI/ACSL for specifications, libjsonschema/OpenAPI Generator/VeCoGen for generation, PC‑lint Plus/Frama‑C for verification, and CMake/Git for recursive refinement.

Expected effort reduction ranges from 20‑60% depending on project type. The methodology is particularly valuable for safety‑critical systems (through formal verification) and interface‑heavy codebases. The pilot implementation requires minimal upfront investment and serves as a practical starting point for teams adopting this approach.