Formal

Role Description You’ll contribute to formal verification efforts for a new low-level programming language. Expect to architect, write, and review formal specifications and complex mechanized proofs in Rocq. You will work closely with engineering teams to extract correct-by-construction software from mechanized proofs. Responsibilities - Lead the design, development, and maintenance of mechanized theorems and proofs in Rocq. - Collaborate closely with the compiler and OS teams to understand design goals, define formal specifications, and integrate verification into the development lifecycle. - Participate in both sides of code reviews. - Actively anticipate and communicate future roadblocks. Qualifications - Advanced degree in formal methods or programming languages or equivalent practical experience. - Deep expertise and extensive practical experience with Rocq and its ecosystem (tactics, libraries, automation). - Experience leading or contributing to complex formal verification projects such as compilers or OS kernels. - Ability to formally articulate, reason about, and verify low-level security, safety, and correctness properties of programming languages like Rust and C/C++. - Ability to read, write, and understand formal programming language specifications and implementations. - Ability and willingness to document, teach, and explain complex technical problems and solutions. - High level of independence and autonomy. Benefits - Compensation is comprised of a stock grant (≥ 0.2%) conditioned on a vesting schedule. - Unlimited paid and unpaid vacation time. - Reimbursable vacation expenses (transportation and lodging up to $1k). - A triennial $4k computing device allowance. - Comprehensive medical, dental, and vision insurance. - $120 monthly gym allowance. - $250 yearly to spend on anything educational.

Role Description You’ll lead the development of a new, Rust-like programming language intended to run in kernel-space. Expect to write and review design documents, implementation decisions, lots of code, machine-checked proofs, and LaTeX specifications. - Develop an existing compiler codebase and software to continuously test and verify its correctness - Formally verify language properties and implementations - Collaborate and co-design with OS and networking teams to tightly integrate the language into the overall product - Participate in both sides of code reviews - Actively anticipate and communicate future roadblocks - Participate in the open-sourcing of the language Qualifications - 3+ years of software engineering experience - Deep understanding of type systems and logic systems: formal specification, design, implementation, and trade-offs - Experience with formal programming language semantic specifications, proofs, and ability to translate them into code - Experience with formal verification including model checking, theorem provers and SMT-based approaches - Understanding of system-level language concerns such as binary formats, loading, ABIs, linking, and machine targets - Mastery of or ability to quickly master Rust - High level of independence and autonomy - Ability and willingness to document, teach, and explain complex technical problems and solutions Benefits - Compensation is comprised of a competitive market salary and stock grant (>= 0.4%) conditioned on a vesting schedule - Unlimited paid and unpaid vacation time - Reimbursable vacation expenses (transportation and lodging up to $1k) - A triennial $4k computing device allowance - Comprehensive medical, dental, and vision insurance - $120 monthly gym allowance - $250 yearly to spend on anything educational