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

Beneficial AI Foundation

The Beneficial AI Foundation aims to keep AI beneficial for generations to come. It supports a broad range of technical AI safety research though staff research, university partnerships and its Buterin Fellowship program.

https://www.beneficialaifoundation.org/
Previous
Previous

Growth and Marketing Operations / Analytics Specialist

Next
Next

Machine Learning Infrastructure Engineer