Formal Methods Engineer, Proof Automation

Full Time
Boston, MA
Posted 7 months ago

Full time
Boston, MA

The Current State

Businesses should be built on a rock-solid foundation. However, the current edge and cloud computing infrastructures are built on a foundation of sand. None of its components should be considered “trusted.” Design and implementation defects in these components give rise to vulnerabilities that can become critical security flaws. And security flaws become safety issues and can severely impact governments and entire industries.

BedRock’s Mission

Our Mission is to BedRock the world’s critical systems from Edge to Cloud, implementing the most secure and Trusted Compute.

THE FUTURE IS BUILT ON BEDROCK – An Unbreakable Foundation for Formally Secured Computing. An Unbreakable Foundation for Formally Secured Computing. BedRock Systems is on a mission to deliver a trusted computing base from edge to cloud, where safety and security isn’t just a perception, it’s a formally proven reality. Our foundation does not require painful up-stack changes; it embraces existing hardware, operating systems, and application ecosystems. When systems are BedRocked, the operation is secured, innovation is unlocked, new services are launched, trust is re-established, and revenue can grow. Governments and businesses gain back velocity and can securely evolve at the speed of software.

Our Team Is Growing!

BedRock Systems is a stealth startup with a global team. Our platform is based upon cutting-edge technology and leverages the latest development methodologies and tools. We were founded by industry veterans who built large successful companies from scratch. Our top-notch team is a mixture of the best from industry and academia. Come transform the computing landscape. Join the BedRock Systems team!

As a BedRock Formal Methods Engineer you: 

  • Are an expert in automated verification of large C++ codebases to speed up our “code-to-proof” loop by optimizing and improving our automation tooling
  • Will pitch into developing proofs (40%) as well as automating the process (60%)

You could be a great fit for this role if you have:

Must Haves:

  • Coq expertise, especially Ltac / Ltac2 / plugins and deep knowledge of proof terms
  • Built automation for various domains
  • Comfortable with Ocaml
  • Exposure to separate logic
  • Exposure to C/C++

Nice to Have:

  • Contributed to the development of Coq itself, or plugins
  • SMT / SAT solver expertise
  • Experienced with Iris, possess concurrent systems expertise
  • Kernel / operating systems experience

Related Skills:

  • Automated theorem proving techniques, e.g., resolution, superposition, etc.
  • Invariant inference
  • Static analysis
  • Verified / trustworthy / high-assurance software engineering

Why BedRock?

We were founded by industry veterans who built large successful companies from scratch. Our top-notch team is a mixture of the best from industry and academia. Come transform the computing landscape.

BedRock is an equal opportunity employer. We celebrate diversity and are committed to creating an inclusive environment for all employees.

Job Features

Job CategoryResearch & Development

Apply Online

Share This Job Posting

Share on linkedin
Share on facebook
Share on twitter
Share on email