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. Every harness below carries either the time a solver took to discharge it or the memory ceiling that stopped it. Six earlier harnesses carried neither, because they proved nothing; in September those were deleted rather than counted.
VERIFICATION:- SUCCESSFUL line this machine actually produced, with the solve time printed below wherever one was measured. Four do not, and are listed as unsolved rather than as pending. Seventeen guard tests mutate each property’s oracle and assert the property then fails — a proof that cannot fail proves nothing.
Bounds printed
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 | 11 solved Kani harnesses of 15; 5 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.
Note what our own cell does not say. It does not say fifteen harnesses; it says the eleven that a solver actually discharged. The other four are named in the proof section, with the memory ceiling that killed each one.
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. Fifteen harnesses are authored in oxiautors-formal. Every row below is one of exactly two things and nothing in between: a solve this project’s machine actually performed, or an honest “authored, not solved here.” Where a run was timed, the wall time is on the row; the two E2E harnesses were discharged in an earlier round and carry a verdict without a re-measured time. Machine: 24 GB shared, CBMC capped at 7 GiB resident and 40 minutes per run.
Solved — 11 harnesses with a measured VERIFICATION:- SUCCESSFUL
WatchdogTimer, not a model of one. Symbolic tick values bounded to 64 ns. Stated as an iff, so a one-sided implementation cannot satisfy it.MpuRegion::validate accepts a descriptor iff the hardware could actually program it — size a power of two, base aligned to it.--solver minisatThe real freedom-from-interference result. PartitionTable::insert rejects a candidate iff it overlaps an admitted partition — both directions, against an independently written oracle, with every partition’s ASIL left symbolic over Qm..=D. It asserts the strictly stronger “no admitted pair shares an address,” of which the ASIL-D case is a subset.kani::unwind(9) on the CRC loop.data_id_list.Authored, not solved on this machine — 4 harnesses
Runtime Symex 574 s, 4.57 M program steps, 145,819 VCCs. The bottleneck is program size, not input domain: slice-iterator walks in the state observer, which CBMC expands with a pointer check per iteration. Two fixes are identified and untried.The three OSEK harnesses call the same trace runner and differ only in which counters they assert, so their solve costs are near-identical. Solving one would be a strong indication about the others and not a verification of them. This page will not blur those two.
Kernel-checked lemmas — oxilean
SenderReceiverPort.VfbRouter.oxilean 0.1.2 reduced a Nat bit-operation only when both arguments were already literals, so the CRC fold was stuck at its first step. 0.1.3 lifted that, and the kernel now reduces the full 96-step CRC32P4 fold (poly 0xF4ACFB13 applied reflected) over the CRC-covered bytes of a protected E2E frame. Discharged at a concrete frame — a closed rfl — not universally quantified over payloads. The ∀-form is still not dischargeable, and the module says so and demonstrates it against the live kernel.Here is what changed since the last version of this page, which said nine of nine passing. An adversarial review went back through those nine and found that six of them proved nothing. Three drove a WatchdogState enum that exists nowhere in the product — the shipped crate exposes WatchdogTimer and SupervisionMode and never that type — and two of those three were not even symbolic. The three OSEK harnesses were tautologies: one asked the solver to prove ¬(A ∧ B) inside a branch that had already falsified A; one fed a three-task array whose last two entries were ready = false; one computed the exact predicate it then assumed and asserted. There was no resource, no acquire, no release and no blocking anywhere in that file, so “no priority inversion” and “no deadlock” were not being modelled at all. All six are deleted.
A second review, the same day, found something worse: some of the replacement source files carried solve results this machine had never produced. A comment above the OSEK harnesses read “MiniSat solves them well inside the budget.” An independent run was killed at 7,219 MB. That comment is now a SOLVE STATUS: NOT SOLVED line naming the measurement that refuted it. Two documented “falsifying mutations” also turned out not to falsify anything, and were replaced with mutations that do — each one pinned by a guard test that runs the harness’s own property against the mutated oracle and asserts it fails. All fifteen harnesses now carry one.
The OSEK model’s correspondence to the shipping kernel used to be prose, which meant a kernel change could silently invalidate the harnesses. It is now executable: oxiautors-bsw-os is a dev-dependency of the formal crate, and every trace of the bounded search is replayed through the model and through the real Scheduler and resource::{get_resource, release_resource}, comparing the verdict, the error class, the running task, every dynamic priority, every held-resource LIFO and the ready-queue occupancy after every step — 243 configurations × 6,561 four-action traces. Within that bounded space the priority-ceiling properties are statements about the shipping kernel, not only about a model of it. It does not discharge the three unsolved harnesses, and it is bounded exactly as its own constants say.
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. Sixteen further Kani harnesses live in oxiautors-core, oxiautors-rte and oxiautors-fusa; this project’s measurement log records no CBMC solve for any of them, so none is counted above.
Nothing in this section contradicts the section above. The eleven solves are real and the four failures to solve 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: oxiautors-cloud, oxiautors-python, oxiautors-twin and oxiautors-hil are between 36 and 43 lines each — unchanged by the September work. 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 oxiautors-formal; the Kani compiler and CBMC themselves come from cargo kani setup, and a fresh CI runner has to repeat that. And cargo kani -p oxiautors-formal with no filter is no longer a sub-30-minute job, because one solved harness alone costs 833 seconds.
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.
Payable in advance. Source access within one business day of receipt.
Credited in full against a Platform or Programme licence. Complete workspace, all verification artefacts, and the status section above in full detail. Non-commercial evaluation 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.
The proofs were the defect. We went looking, and we found it in our own work.
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 a supplier does when the verification turns out to be the thing that is broken. In July we installed Kani and found two harnesses that had never executed at all — one orphaned from the module tree, one with an unbounded unwind that ran forever. We fixed those and published nine of nine. In September we went back and asked a harder question: not do they run, but do they prove anything. Six did not. They are deleted. Then we asked the same question of the replacements, and found source comments asserting solve results no machine here had produced. Those are corrected, and the measurements that refute them are quoted in the source.
Every one of those defects was in our verification rather than in the product, and every one was invisible for as long as nobody adversarially reviewed it. That is the entire argument for this page existing in this form.
That is why solve times are printed on this page instead of a claim of formal verification. A bounded proof that tells you its bounds — eight-byte buffers, sixty-four-nanosecond windows, four-action traces — is worth more to a safety case than an unbounded claim that does not. And a harness listed as unsolved is worth more than one listed as passing on the strength of a comment nobody checked.
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, occasionally the four harnesses that do not solve. 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.