Founder of dbit.one. I write the architecture myself and stay with the project until it ships — you get the engineer who wrote the code, not an account manager with a deck.
Client systems are under NDA. Everything below is open, so you can read it instead of taking my word for it.
Correctness of systems that are hard to be sure about, and cheap ways to find out you were wrong. The repositories share one assumption: a green run carries no information until something has tried to make it red.
| alibi | Reverts your change, reruns the tests your agent just wrote, reports the ones that never went red. No model, no network, any test runner. |
| unflake | Deterministic simulation testing for TypeScript. One seed, one byte-identical run; a found bug shrinks to a minimal schedule. |
| bulwark | Raft under seeded partitions and crashes. All five safety properties from the paper checked on every transition, every client history verified linearizable. |
| adya | An MVCC engine with four isolation levels including Cahill's SSI, and a dependency-graph checker validated against PostgreSQL. |
| pnueli | An explicit-state model checker: symmetry and partial-order reduction, liveness under weak fairness, every reduction validated against the unreduced search. |
| sable | A programming language — lexer, parser, AST compiled to closures. Its own lexer and parser are written in Sable. Try it in a browser. |
Each one is convicted by something that could have disagreed with it: a museum of bugs that must be caught one by one, an exhaustive search running beside the reduced one, PostgreSQL as an outside arbiter, a test suite that has to go red on purpose before it counts.
Engineering write-ups, in Russian, on Habr — including the one about my own test harness finding a bug in my own Raft implementation, and the one where the whole core of a language was rewritten and not one of 444 golden files moved.