Software Engineer
Beneficial AI Foundation
📍Remote (Global) 🕔 Full Time
💰 $70,000—$150,000 USD 🔄 Rolling Applications
This position involves working with Bryan Parno, Max Tegmark and colleagues at the Beneficial AI Foundation on turbocharging formal verification of Rust code with AI tools as described here and in Towards Guaranteed Safe AI (a high-level introduction is given in the 2nd half of this TED talk).
Key Responsibilities:
Develop and maintain core features of the Verus verification tool for Rust
Improve efficiency of LSP (language server protocol) implementation Verus Analyzer
Implement a tool for exporting Verus proof obligations to the Lean theorem prover
Work closely with Prof. Bryan Parno (CMU) from the Verus team on above goals
Contribute to advancing AI safety through the application of formal verification methods
Ideal Candidate:
Strong software engineering background
Very strong at Rust programming
"Verification curious": eager to learn about formal verification techniques for making provably bug-free code
Self-motivated, comfortable working independently and collaboratively with academic and research partners
Eager to contributed to free open-source tools ensuring that code does what we want it to do