LLMs draft code; Dafny, FDR4, and Isabelle — formal verification suites for deductive proof, model checking, and theorem proving — certify it.
A brake controller is not the place to put a stochastic generator. Vibe coding, in the safety-critical sense, means letting an LLM translate a natural-language requirement directly into source code, and it runs into a wall the moment that code has to be certified.
In her July 2026 EE Times analysis, Intel principal engineer Beenish Zia flags that this definition is narrower than the looser "describe what you want and ship it" usage popular elsewhere (EE Times). For a brake controller, an avionics module, or an infusion pump, that distinction is load-bearing. Functional-safety standards such as DO-178C for aviation, IEC 61508 for industrial controls, ISO 26262 for automotive, and IEC 62304 for medical-device software require deterministic, traceable, qualified evidence that the code does what the requirements say it does. A stochastic generator, by construction, cannot produce that evidence.
The SUSVIBES benchmark, published by Danqing Wang and colleagues, ran SWE-Agent with Claude 4 Sonnet against 200 real-world open-source tasks that had previously yielded vulnerable human implementations. The agent produced functionally correct code 61% of the time, but only 10.5% of its solutions were secure (arXiv:2512.03262). Augmenting the agent with vulnerability hints did not close the gap. For software where a missed bounds check can become a recall or a crash investigation, a 50-point functional-versus-security spread is the wrong shape of number.
The engineering response in 2026 is converging on the same architecture. Zia's piece proposes a hybrid: the LLM drafts code from requirements, deterministic static and dynamic analysis tools sit in a feedback loop, and the diagnostics they emit become repair prompts the AI agent acts on. Once the quality gates pass, a human expert reviews the result. Her stated rule of thumb: AI-generated code is acceptable in safety-critical systems only when it is subjected to the same verification and validation as human-written code (EE Times).
The Forge pipeline, published in June 2026 by Ran Wei and co-authors, makes that loop concrete. Forge guides an LLM's Java output through a Model-Driven Engineering chain to three complementary verifiers: Dafny for deductive verification, FDR4 for CSP refinement checking, and Isabelle/Z-Machines for theorem proving (arXiv:2606.22413). Each verification failure is converted into a structured correction prompt; the LLM is the draft generator, the MDE chain is the discriminator, and the paper maps the whole loop onto DO-178C, IEC 61508, and ISO 26262. The certifiable artifact in this design is the verification loop itself, not the model behind it.
That framing matters because it puts the qualification burden where it can actually be met. A standard like ISO 26262 does not care whether the source code was written by a person or an LLM; it cares that the tool chain that produced and validated the code is itself qualified, that requirements are traceable bidirectionally to implementation and test, and that the verification evidence is reproducible. A closed-loop pipeline built on Dafny, FDR4, and Isabelle is, in principle, as qualifiable as any other deterministic tool chain. A raw LLM call is not.
The honest counterargument is that any non-trivial verification loop is itself a tool that has to be qualified under the same standard, and that the Forge paper reports pre-peer-review results on a specific Java subset rather than a deployed automotive program. The SUSVIBES 10.5% secure-solution rate is a preprint benchmark, not a regulator's finding, and Zia's hybrid model is an engineering position, not an audited methodology. None of that changes the underlying shape of the answer: the certifiable thing is the loop, and the model sits inside it as a draft generator, never as the gatekeeper.
For engineering teams writing next to a brake controller or a flight-control surface, the practical split is straightforward. Use vibe coding on non-safety code, on tooling, and on the scaffolding around a safety-bearing module. For anything failure-cost-bearing, treat the LLM as a junior developer whose output has to clear the same static analysis, formal verification, and human review as everyone else's, and document that chain so an auditor can read it. The cockpit door is not metaphorical. It is a verification boundary.