A Pure Rust AUTOSAR Classic and Adaptive platform in one workspace — RTE, VFB, OSEK OS, MCAL, BSW, ara::com, ara::crypto, UDS, SOME/IP and Uptane OTA. In our own competitive table, the formal-verification row reads "None" for all three incumbents. Ours reads what it actually is, bounds included.
This is our own competitive table, reproduced with the row that goes against us left in. Three of the four axes favour Rust. One does not, and it is the one a Tier 1 will ask about first.
| Platform | Language | Memory safety | ISO 26262 ASIL-D | Formal verification | Classic + Adaptive |
|---|---|---|---|---|---|
| AUTOSAR Classic | C | Manual | Established | None | Classic only |
| Adaptive AP | C++ | RAII only | Partial | None | Adaptive only |
| Vector MICROSAR | C / C++ | Manual | Certified | None | Separate products |
| OxiAutors | Rust | Compile-time | Not certified | 9 Kani harnesses, 4 kernel-checked lemmas | One workspace, partial spec coverage |
MICROSAR is certified and OxiAutors is not. There is no version of that sentence that helps us, so it is at the top of the page instead of the bottom. What the table does show is that the formal-verification column is empty for all three incumbents, and that Classic and Adaptive being separate products is a procurement fact rather than a technical necessity. Whether those two things outweigh a certificate is your decision, and it depends entirely on where you are in the programme.
Classic and Adaptive against the same core types, in one workspace, with one build.
Formal verification is the easiest thing in this industry to imply and the hardest to check. Nine harnesses run under Kani 0.67.0 and CBMC 6.8.0, and all nine pass in about nineteen seconds. Six are exhaustive over their input domain. Three are bounded, and here are the bounds.
Kernel-checked lemmas — oxilean
Two of the nine Kani harnesses did not work when we first ran them. kani_wdt.rs was an orphaned module that had never been compiled since the day it was written. kani_e2e.rs had an unbounded CBMC unwind and never terminated. Both were real defects in our own verification, and both were invisible for as long as the harnesses were written and never executed. We are telling you this because the industry standard for a page like this is to report the nine and not the two, and because if you are buying verification you should want a supplier who ran it.
oxilean is an in-house, homegrown pure-Rust prover and kernel for the Calculus of Inductive Constructions. It is not the Lean 4 toolchain and has no relationship to mathlib; lean and lake are not installed anywhere in this project. proof_certificate.rs renders certificate text — it is a document generator, not an attestation service.
Nothing in this section contradicts the section above. The proofs are real and the bounds are real. What does not exist is anyone official who has agreed with us.
Four crates in the workspace are placeholders and should not be counted as capability by anyone evaluating this: oxiautos-cloud, oxiautos-python, oxiautos-twin and oxiautos-hil are between 36 and 43 lines each. They are in the crate list because removing them would be a different kind of dishonesty. Also note that the kani-verifier crate in Cargo.lock is the crates.io shim, a dev-dependency of oxiautos-formal; the Kani compiler and CBMC themselves come from cargo kani setup, and a fresh CI runner has to repeat that.
Vector quotes MICROSAR on application. That means you cannot find out whether an AUTOSAR platform is affordable without first telling a competitor's sales team what you are building. Annual terms, per vehicle programme, invoiced once.
Complete workspace, the nine Kani harnesses, the oxilean attestations and the status section above in full detail. Non-commercial use only. No sales contact unless you ask for it.
Source licence for one vehicle programme, unlimited ECUs and unlimited units. Verification artefacts regenerated per release: the Kani run log with its bounds, the oxilean attestations, and a CycloneDX SBOM. Five business day response.
All vehicle programmes, a named engineer, participation in your ISO 26262 work products, and support for the version you ship for the vehicle lifetime. Source escrow on request.
Priced per vehicle programme — not per ECU, not per unit, not per seat. No royalty on vehicles shipped, no runtime fee, no audit clause. The number is on this page because the incumbent's is not, and because you should be able to work out whether this is affordable before you tell anyone what you are building. What the number does not buy is a certificate. Read the status section again before you decide it is a bargain.
Two of the nine had never run. We found out by running them.
The other products in this ecosystem close this page with a stack tree — nine years of replacing C, one layer at a time, until there was nothing foreign underneath. OxiAutors contains almost none of that stack. It takes one crate from the ecosystem, oxilean, and otherwise stands on RustCrypto and rustls. The RTE, the VFB, the OSEK scheduler with its timing protection and priority ceilings, the MCAL layer, the E2E profiles and the whole ara:: stack were written in this workspace against the AUTOSAR documents.
So the provenance claim here is not about depth. It is about what happens when someone actually runs the verification. Nine Kani harnesses had been written for this workspace. When we installed Kani 0.67.0 and CBMC 6.8.0 and ran them, two did not work: kani_wdt.rs had never been compiled since the day it was authored, and kani_e2e.rs had an unbounded unwind that ran forever. Both were real defects, both were in our own verification rather than in the product, and both were completely invisible for as long as the harnesses existed but were never executed. All nine pass now.
That is why the bounds are printed on this page instead of a claim of formal verification. Six of the nine cover their entire input domain. Three cover a bounded one — eight-byte buffers, four-kilobyte partitions — and a bounded proof that tells you its bounds is worth more to a safety case than an unbounded claim that does not.
Most of the ecosystem is public on GitHub under Apache-2.0. The AUTOSAR platform is the part we licence.
Most conversations about this platform end on one line of the status section — usually the certification row, sometimes the MCAL coverage for a specific part. Send that line and the ECU you have in mind. You will get back what is implemented for that target, what is not, and whether the honest answer is that you should buy MICROSAR this programme and talk to us about the next one. One business day, no qualification call.