Generative AI guesses; safety-critical systems can't. Apkallu Labs wraps large language models in formal verification — building a full-stack verified ecosystem from the code that flies aircraft to the cloud infrastructure that trains the models.
A language model produces the most plausible answer, not a guaranteed one. Plausible is fine for a chatbot; it is unacceptable for a brake controller or a production IAM policy.
The method
Proof as the gatekeeper
Every AI-generated artifact — a C function, a Terraform plan — must discharge formal proof obligations before release. A hallucination can't get past a proof obligation.
The standard
Built for the strictest rooms
Designed against DO-178C, ISO 26262, and the security baselines regulated infrastructure demands. If the logic doesn't hold, nothing ships.
Now building · Verifier Workbench
Proves whether C code is safe, and shows exactly where it isn't.
Verifier Workbench puts the Prover-in-the-Loop to work on C code today. Each function is checked by a bounded model checker over a real SAT or SMT solver. Every refuted obligation comes with the inputs that break it, and a model's fix counts only when the checker proves it removes the defect and changes nothing else.
A live run on arith.c: CBMC 5.95.1 over Z3 4.8.12 refutes two obligations in 0.12 s. The sum in avg() overflows at a = b = −2147475457, and store() writes buf[16], one past the end of the array. Each finding carries the inputs that break it, in decimal and hex, and the path that reaches it.
Repair asks a model for a patch, then checks it mechanically. Here the first attempt is rejected: the behavior proof shows store(idx = 13, v = 128) would leave buf[13] different. The second widens the sum and tightens the guard; CBMC re-verifies it and proves both functions behave as before wherever the original was well-defined.
Each run gets a printable report: the checks and loop bound that applied, each proof obligation with its status, the counterexamples, the patch that held and every attempt it took to get there. Print it or save it as PDF.
Each product stands alone; together they form a verified stack — the logic that runs your systems, the infrastructure it runs on, and the expertise to operate both.
The logic layerApkallu Studioapkallu.studio
AI-generated safety-critical software
Write the formal contract; Studio's generate-and-prove loop produces an implementation that SMT solvers verify against it — then generates the MC/DC test vectors and certification evidence to match.
Deductive proof of code correctness, ACSL contracts, portfolio SMT solving
Automated MC/DC vectors with gap analysis — 100% coverage, generated not guessed
C with MISRA C:2012 today; Ada/SPARK and Rust on the roadmap
Describe infrastructure in natural language; Cloud generates the Terraform and Kubernetes manifests — and proves every plan against your security and compliance policies before anything is applied.
Infrastructure as intent: natural language in, verified manifests out
Policy-as-logic checks on every plan — encryption, network exposure, least privilege
GPU orchestration and elastic scale for AI workloads, drift re-verified continuously
Hands-on expertise for the hard parts: on-prem cluster design and operations, documentation that is actually runnable, and strategy for putting AI to work without betting the company on a guess.
On-prem and air-gapped cluster design, build-out, and management
Living documentation and executable playbooks, not shelf-ware
AI-adoption consulting grounded in verification-first engineering
Standard LLM pipelines stop at "looks right." Ours wraps the model in a formal verification layer, so nothing leaves the loop without a proof — and every rejection makes the next attempt smarter.
01Intent
You describe the need
A function contract, an infrastructure requirement, a policy constraint — stated once, formally.
02Synthesis
The model proposes
A fine-tuned LLM drafts candidate code or configuration, constrained by the contract and coding standards.
03Proof
The solver decides
SMT solvers check the candidate against every obligation. Invalid? The counterexample drives automatic repair. Valid? Correctness is proven, not sampled.
04Release
Evidence ships with it
Proof logs, coverage, and traceability come out of the pipeline as first-class artifacts — ready for auditors, certification authorities, and your own postmortems.
AGENT · arith.cliveCBMC 5.95.1 · z3 4.8.12
F-01avg · line 5 · overflow · a=-2147475457 b=-2147475457
F-02store · line 13 · bounds · idx=16 v=0
iter 0 · verify · 2 refuted · 0.13 s
iter 1 · repair → rejected (behavior changed) · 0.49 s
store(idx = 13, v = 128) is well-defined in the original, but the global buf differs at buf[13] (original: 128, patched: 0).
iter 2 · repair → re-verify · all 3 proved ✓ · 0.49 s
Verified — patch held (re-checked by CBMC).
≡ avg behaves as before (proved)
≡ store behaves as before (proved)
0 refuted3 proved
The loop on arith.c, as the Workbench logged it: the first patch changes what store() does and is rejected with a counterexample; the second is proved.
Research
The questions we're working on.
Synthesis
Counterexample-guided repair
Turning solver counterexamples into structured repair prompts that converge — measuring iteration counts, not vibes, on a public benchmark of safety-critical leaf functions.
Coverage
Coupled conditions in MC/DC
Unique-cause MC/DC provably cannot isolate logically coupled conditions. We're building masking-MC/DC analysis that covers them soundly instead of flagging them and moving on.
Infrastructure
Policy as logic
Encoding cloud security baselines as machine-checkable obligations, so "no public buckets, ever" is a theorem about the plan — not a linter rule someone can silence.
Careers
Small team, unforgiving standards.
We hire people who think a counterexample is good news. Remote-friendly, headquartered in Renton, Washington.
Formal Methods Engineer
Frama-C/WP, SMT solving, and the taste to keep specifications honest.
