A Focused Research Organization working on AI oversight via formal methods
Berkeley, CA
Joined February 2026
- Tweets10
- Following1
- Followers260
- Likes2
Pinned Tweet
We're hiring! Come help us build tools for overseeing powerful AIs oath.tech/jobs/
New: Lean-ux, an executable Lean mirror of several Linux subsystems, built by testing against instrumented Linux running in QEMU
+ Lean proofs of properties for the Wireguard mirror,
+ early experiments trying to prove the mirror correct vs the binary
github.com/OathTech/lean-ux-…
We built a Lean port of Cerberus, a highly realistic C semantics. If you want to model and reason about C code in Lean, now you can github.com/OathTech/cerberus…
Yes this is definitely a prototype. Expect edge-case bugs & please don’t use it to verify your production flight controller or anything
cute semantics :) It's a shame it's buggy though :\
I hope you haven't used it to prove anything big yet!
It's kinda hard to trust vibe-coded semantics IMO even testing isn't enough to catch all the bugs
ALT pathleak2.c next to the Lean theorem pathleak2_every_outcome and two terminal outputs. cerberus-lean runs the program to Defined, value Specified(0), with empty stdout. The same program compiled with gcc prints hunter2 and fails the assertion n == 0.
Formal Methods Research Engineer jobs.lever.co/convergentrese…
Research Engineer, Tools & Infrastructure jobs.lever.co/convergentrese…