@oath_tech

A Focused Research Organization working on AI oversight via formal methods

 Berkeley, CA
oath.tech
Joined February 2026
  • Tweets8
  • Following1
  • Followers251
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
2
17
3,192
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
2
114
11,454
Yes this is definitely a prototype. Expect edge-case bugs & please don’t use it to verify your production flight controller or anything
Kiran@kirancodesSep 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,017
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
435
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
356
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
291
Load more