I’m Baris Erdem. I build systems software and verification tooling.

Some of what I’ve worked on:

  • attest, an AI verification gate: it generates TLA+ specifications from source code and execution traces and model-checks them, so you catch the concurrency and consensus bugs that tests and type systems miss.
  • lockstep, a concurrency-testing framework for the BEAM (DPOR, PCT, and deterministic replay).
  • A handful of Ada/SPARK formal-methods libraries.

Reach me at baris@erdem.dev.