Determinism is not a feature — it is the architecture
In the floating-point world, the same scenario yields different results on every processor; model error, malfunction and cyberattack become indistinguishable. We built the entire stack on one principle: same input → bit-identical result on every machine.
Four layers of assurance
Guarantees checked in the language
16 effects (saf, deterministik, sınırlı/WCET, tahsis_yok, panik_yok…) are machine-checked in the BERK language; purity is transitive across the call graph. A violated contract stops the program before it runs — berk kontrol is the same gate for CI.
Comprehensive automated testing
280+ core language checks, 1,642 signed-package tests (BerkROS/AI/Finance/Bio/RTOS), ~1050 digital-twin tests and 681 dds:: safety-math tests — re-run on every change, on every platform.
Formal verification (TLA+)
Concurrency, deadlock and timing were handed to the TLC model checker, which walks every reachable state: 18.4M states in Hard RT Core, 5.1M+ in Berk DT — zero violations.
Differential equivalence gate
The field-going .berk source and its Rust mirror are compared on shared vectors in every CI run; integer/boolean outputs must be bit-identical. Any drift = a red test.
The invisible cost of the float world
| Floating-point world | The LL BERK approach | |
|---|---|---|
| Same scenario, different machine | Different result — depends on CPU/compiler | Bit-identical state_hash |
| Malfunction vs. cyberattack | Indistinguishable; thresholds get loosened | Clean break signal at the first frame |
| Post-incident analysis | "Could not reproduce" | Exact replay with a single command |
| Audit / certification | Evidence production is separate, costly work | Hash logs, replay certificate, deviation report built-in |
| Tampering | May go unnoticed | The hash chain breaks instantly |