Pinned Tweet
Oath Technologies@oath_tech
Sep 9
We're hiring! Come help us build tools for overseeing powerful AIs oath.tech/jobs/
3
5
17
3,424
Oath Technologies@oath_tech
Oct 22
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-…
1
3
11
522
Oath Technologies@oath_tech
Oct 22
Replying to @oath_tech
This is research-ware. Expect many bugs and do not use it in consequential environments
0
0
0
67
Oath Technologies@oath_tech
Sep 26
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/cerbe…
2
21
114
11,538
Oath Technologies@oath_tech
Sep 27
Replying to @oath_tech
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.
1
2
14
1,038
Oath Technologies@oath_tech
Sep 27
Replying to @oath_tech
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
441
Oath Technologies@oath_tech
Sep 9
Replying to @oath_tech
Formal Methods Research Engineer jobs.lever.co/convergentrese…
1
2
1
362
Oath Technologies@oath_tech
Sep 9
Replying to @oath_tech
Research Engineer, Tools & Infrastructure jobs.lever.co/convergentrese…
0
1
2
295
Load more