Umwelt trains AI models to verify hardware.
We train our own models to read a chip design and its specification, and to write the properties the design must satisfy. Every property they write goes to a formal engine, which returns a proof or a counterexample.
That verdict is exact, so we use it as the training signal. Our models are rewarded for properties that hold and that catch real bugs, and penalised for false alarms.
The name comes from Jakob von Uexküll, a biologist who used the word Umwelt for the part of the world an organism can perceive.
Design tools can check a property once it is written. Deciding what to check is still done by hand, by specialists, and it is where bugs slip through. That is what our models learn to do.
We built First Silicon, a benchmark of 86 real bugs that engineers fixed in open-source chip designs, judged by an exact formal checker. The best frontier model we tested catches 16 of them without a false alarm. Most bugs escape every model.
| Opus 5.5max effort | Opus 5.5default | Fable 5.1 | Sonnet 5.5 | Haiku 5.5 | |
|---|---|---|---|---|---|
| Caught, zero false alarmsSTRICT · all 86 bugs | 18.6%16 / 86 | 14.0%12 / 86 | 9.3%8 / 86 | 8.1%7 / 86 | 3.5%3 / 86 |
| Without defective promptsSTRICT · 80 bugs | 17.5%14 / 80 | 15.0%12 / 80 | 10.0%8 / 80 | 8.8%7 / 80 | 3.8%3 / 80 |
| OpenTitanSTRICT · 70 bugs | 15.7%11 / 70 | 12.9%9 / 70 | 5.7%4 / 70 | 5.7%4 / 70 | 1.4%1 / 70 |
| Other open-source projectsSTRICT · 16 bugs in 10 projects | 31.3%5 / 16 | 18.8%3 / 16 | 25.0%4 / 16 | 18.8%3 / 16 | 12.5%2 / 16 |
| Caught, false alarms allowed86 bugs | 32.6%28 / 86 | 25.6%22 / 86 | 15.1%13 / 86 | 10.5%9 / 86 | 3.5%3 / 86 |
| Precision of alarmstrue alarms / all alarms | 34%49 / 145 | 32%34 / 105 | 22%21 / 94 | 32%15 / 47 | 21%6 / 28 |
| False alarm on the fixed designbugs · lower is better | 31.4%27 / 86 | 25.6%22 / 86 | 24.4%21 / 86 | 12.8%11 / 86 | 9.3%8 / 86 |
| Fixed after June 2026STRICT · 3 bugs, after training cutoff | 0 / 3 | 0 / 3 | 0 / 3 | 0 / 3 | 0 / 3 |
We are hiring researchers and engineers in machine learning, reinforcement learning, formal methods and hardware verification. We also work with design teams who want to test our models on their own RTL.
Working on a chip that has to be right the first time, or want to work with us? Write to us below, or at contact@umwelt.vision.