Oath Technologies@oath_tech

A Focused Research Organization working on AI oversight via formal methods

 Berkeley, CA
oath.tech
Joined February 2026
We're hiring! Come help us build tools for overseeing powerful AIs oath.tech/jobs/

Jobs at Oath Technologies

Oath Technologies is hiring research engineers in Berkeley, California.

oath.tech
3
5
17
3,331
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-…

GitHub - OathTech/lean-ux-proto

Contribute to OathTech/lean-ux-proto development by creating an account on GitHub.

github.com
1
3
8
439
This is research-ware. Expect many bugs and do not use it in consequential environments
48
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…

GitHub - OathTech/cerberus-lean: A fork of Cerberus C adding a Lean 4 port of the semantics

A fork of Cerberus C adding a Lean 4 port of the semantics - OathTech/cerberus-lean

github.com
2
22
114
11,479
Yes this is definitely a prototype. Expect edge-case bugs & please don’t use it to verify your production flight controller or anything
Kiran@kirancodes
Sep 27
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
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.

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.

1
2
14
1,023
One of the things we’re trying to figure out is how to build trustworthy formal tools using agent labor. Unsolved, seems v hard
1
1
15
436
We're hiring! Come help us build tools for overseeing powerful AIs oath.tech/jobs/

Jobs at Oath Technologies

Oath Technologies is hiring research engineers in Berkeley, California.

oath.tech
3
5
17
3,331
Formal Methods Research Engineer jobs.lever.co/convergentrese…

Convergent Research - Oath Technologies - Formal Methods Research Engineer

About Oath Technologies Oath Technologies is a new research organization building tools for oversight of advanced AIs. As AIs become more powerful, it will become more difficult to understand and...

jobs.lever.co
1
2
1
362
Research Engineer, Tools & Infrastructure jobs.lever.co/convergentrese…

Convergent Research - Oath Technologies - Research Engineer, Tools & Infrastructure

About Oath Technologies Oath Technologies is a new research organization building tools for oversight of advanced AIs. As AIs become more powerful, it will become more difficult to understand and...

jobs.lever.co
1
2
295
Load more