Apkallu Safe Studio by Apkallu Labs Request a demo

Apkallu Labs · The automated aerospace certification factory

Prove-to-Keep
AI Code Generation

Generate. Prove. Keep.
Correct-by-construction code for DO-178C.

An end-to-end AI and formal verification framework built to support DO-178C compliance. Engineers state requirements in plain English; the pipeline is designed to return formally verified C, MC/DC test vectors and a compliance matrix that fills itself in.

Request a demo See how it works

GenerateThe LLM drafts C code and its ACSL contracts.

ProveFormal verification checks every proof goal.

KeepOnly code that passes its proofs is kept.

Built onC + ACSLFrama-CAlt-ErgoZ3CoqKLEEKubernetes

01 — The problem

The AI bottleneck in critical systems

We can't put LLM-generated C code into a flight controller while the AI can't be trusted. Critical systems need certainty, not probability.

Generative AI

Fast, but fallible

Can speed up coding dramatically — but LLMs can hallucinate

Safety-critical systems

No room for error

A single bug could ground an aircraft or lose a satellite

In web development a bug is a nuisance. In aerospace, automotive or medical devices, it can be catastrophic.

The certification bottleneck

Writing code is easy. Proving it won't crash can take years.

DO-178C DAL-A calls for full structural coverage and complete traceability — a heavy investment of budget and engineering time. Verification and certification can end up costing more than development itself, and much of the industry still relies on siloed, manual testing.

02 — The status quo

Traditional certification is failing

To show code is safe, the industry leans on manual verification — including hand-written formal proofs. It's rigorous, but it's hard to scale.

$ $ $ $ Requirements Design Coding Testing Auditing
The DO-178C V-model — cost and red tape at every stage.

Months

it can take to verify code by hand

PhDs

often needed to write the proofs — and they're expensive

Fast but reckless AI. Safe but painfully slow humans.

03 — The paradigm shift

Trust the math, not the LLM.

We don't need a perfect, hallucination-free LLM. We need a mathematical wall behind it: Prove-to-Keep AI Generation.

The idea: let the LLM generate code as fast as it can, then intercept it with an automated formal verification engine. Code is kept only once it's proven — if the LLM hallucinates, the math is there to catch it.

04 — How it works

The AutoCoder pipeline

A systems engineer writes an English requirement. The LLM translates it into C code and mathematical contracts — and an automated formal verification engine decides whether any of it ships.

  1. 01

    Plain-English requirement

    A systems engineer states the intent

  2. 02

    LLM drafts C + ACSL

    Code plus mathematical contracts

  3. 03

    Frama-C SMT solver

    The crucible: every goal must be proven

  4. 04

    Verified code

    Output that has passed formal verification

DESIGNED TO CATCHmemory errorsoverflowslogic flaws

05 — The secret sauce

The surgical feedback loop

Correct by construction Code Math failure Targeted fix

When the LLM makes a mistake, the pipeline is designed to repair it, not fail.

  1. Isolate. The math engine can pinpoint the failing line.
  2. Feed back. Only that targeted failure goes back to the LLM.
  3. Repair. The AI patches its own code and tries again until the proofs hold.

Inner loop: generate → verify with Frama-C / SMT → repair, until the goals are proven. The aim is an AI that acts as its own debugger, in an autonomous, correct-by-construction loop.

06 — Walkthrough · NASA cFS / Fraunhofer

Summing sensor readings

An illustrative example from aerospace sensor management. The AI drafts the code, the verifier flags a potential out-of-bounds read, and the AI corrects its own loop invariant. The goal: code no human had to write, backed by a machine-checked proof instead of trust.

sum_readings.cverified
#include <stdint.h> /*@ requires 0 <= n <= 100; @ requires \valid_read(readings + (0 .. n-1)); @ assigns \nothing; @*/ uint32_t sum_readings(const uint16_t *readings, int n) { uint32_t total = 0; int i; /*@ loop assigns i, total; */ /*@ loop invariant 0 <= i <= 100; @ loop assigns i, total; */ for (i = 0; i < n; i++) { total += readings[i]; ✗ mem_access · \valid_read(readings + i) unproven — nothing bounds i from below } return total; }
Frama-C WP · ✓ all goals proven

Illustrative example · click a step to inspect it.

07 — The solution

A continuous certification factory

This is more than an AI coding tool. We're building a factory designed to automate the DO-178C V-model end to end: feed it human requirements, and it aims to return formally verified code, concrete test vectors and a populated compliance dashboard.

InputEnglish requirements
01AutoCoderCorrect by construction 02Verification crucibleThe outer loop 03Coq CopilotSolving the math problem 04MC/DC + traceabilityEvidence for auditors
OutputGreen audit dashboard

AI generates the code. Mathematics proves it. Kubernetes scales it.

Pillar 1 — Correct by construction

The AutoCoder

Instead of trusting an LLM to write safe code, we use the LLM to write the code and the mathematical constraints it must satisfy.

Requirement

“Return the larger of two sensor readings.”

C + ACSL contract 
/*@ ensures \result >= a &&
            \result >= b;
    ensures \result == a ||
            \result == b; */
int max_reading(int a, int b) {
  return (a > b) ? a : b;
}

The LLM writes the code and its requires / ensures contracts. If a proof fails, it rewrites the code and tries again. Prove-to-Keep: nothing is kept until the math holds.

Pillar 2 — The outer loop

The distributed verification crucible

Formal verification can demand serious compute, so we're turning it into cloud-native infrastructure. Once code is drafted it enters the outer loop, where a Kubernetes Operator schedules and manages verification jobs across a cloud cluster.

formalproof.yaml 
kind: FormalProof
metadata:
  name: sensor-voter
spec:
  source: voter.c
  solvers: [alt-ergo, z3]
K8sCustom Operator
  • Frama-C · Alt-Ergo
  • Frama-C · Z3
  • Frama-C · Alt-Ergo
  • Frama-C · Z3
  • Frama-C · Alt-Ergo
  • Frama-C · Z3

Developers commit a YAML file, and the Operator provisions a cluster of SMT solver pods that aggressively attempt to break the code — formal verification as cloud-native infrastructure.

Pillar 3 — Solving the math problem

The AI Coq Copilot

Traditional solvers can stall on complex non-linear math. When Kubernetes detects a hanging solver, the theorem can be routed to our standalone Coq Copilot, where a tactic RAG database supplies aerospace theorems and proof tactics to the LLM.

  1. SMT solver hangs

    Non-linear math triggers state explosion

  2. K8s reroutes

    The theorem goes to the Coq Copilot

  3. RAG lookup

    Vector database of aerospace theorems

  4. Proof solved

    Step by step in an interactive REPL

When solvers blow up, the system is designed to degrade gracefully to an AI-assisted prover instead of failing.

Pillar 4 — Evidence for auditors

MC/DC generation & traceability

Auditors need evidence. The pipeline triggers KLEE symbolic execution to generate concrete test vectors aimed at full MC/DC — modified condition/decision coverage — and posts each artifact to a central traceability server.

Traceability dashboard · illustrative
ReqRequirementProofMC/DC
HLR-001Sensor voter output✓ Proven✓ Covered
HLR-002Fault detection✓ Proven✓ Covered
HLR-003Input range check✓ Proven✓ Covered
HLR-004Failover timing✓ Proven✓ Covered
KLEE test vectors · illustrative

test001: a=100 b=200 c=300 // no pair agrees test002: a=100 b=102 c=300 // a ≈ b test003: a=100 b=300 c=103 // a ≈ c test004: a=300 b=100 c=104 // b ≈ c

Symbolic execution can find concrete inputs that exercise each condition.

Proving the math is only part of DO-178C. Each artifact is posted to a central traceability server, so the compliance matrix can fill itself in.

08 — The happy path

The end-to-end workflow in action

This is what we believe modern aerospace engineering could look like: an engineer writes a requirement, and the pipeline returns verified code, coverage tests and compliance artifacts.

  1. 01

    Requirement

    Write a redundant sensor voter.

  2. 02

    AutoCoder

    LLM writes C plus its math contracts

  3. 03

    K8s + Frama-C

    Code is checked against its contracts

  4. 04

    KLEE

    MC/DC test vectors are generated

  5. 05

    Dashboard

    Artifacts are linked and published

Requirements in. Verified code, coverage tests and compliance artifacts out.

09 — ROI & the moat

The potential payoff — and the moat

Speed

Potential to dramatically shorten DO-178C development and verification cycles.

Safety & security

Designed to rule out whole classes of defects — buffer overflows, null dereferences, integer overflows and division by zero — by construction.

Cost

Could make formal methods practical without large specialist teams or extensive manual QA — engineers focus on writing good requirements.

The moat

An integrated factory that manual DO-178C processes would find hard to match on speed or cost.

The aim isn't only faster software — it's software that is much harder to break, delivered at lower cost than manual DO-178C processes allow.

10 — The vision

The future vision

We're starting in aerospace because it is among the most regulated industries on earth, with a very high barrier to entry. The same Prove-to-Keep approach could extend to pacemakers, autonomous vehicles, and critical cyber and financial infrastructure.

We aim to build the foundational compiler for the AI software era.

Critical infrastructure Autonomous vehicles Medical devices Aerospace flight control

11 — Early access

Plans that scale with your program.

We're in early access and pricing each engagement to fit. Tell us about your program and we'll follow up with a tailored proposal.

Starter

For small teams evaluating formal verification.

  • A starter allowance of verification runs
  • Core MC/DC generation
  • ARM Cortex-M emulation
  • Community support
  • Standard uptime SLA
Talk to us

Professional

For teams actively shipping certified software.

  • An expanded allowance of verification runs
  • Full MC/DC incl. coupled conditions
  • All emulator targets
  • Certification report templates
  • Priority compute queue
  • Engineering support · enhanced SLA
Start early access

Enterprise

For programs with dedicated requirements.

  • Verification volume sized to your program
  • Dedicated or on-prem infrastructure
  • Custom toolchain integration
  • DER liaison support
  • Dedicated round-the-clock support · custom SLA
Contact sales

Plans are indicative during early access. Early-access partners can lock in launch pricing.

12 — Contact

Let's shorten your certification timeline.

Our team of formal-methods researchers and aerospace engineers can walk your program through the pipeline — with your specifications, on your target.