Riverside Research is an independent National Security Nonprofit dedicated to research and development in the national interest. We provide high-end technical services, research and development, and prototype solutions to some of the country’s most challenging technical problems. All Riverside Research opportunities require U.S. Citizenship Position Overview The Secure and Resilient Systems group seeks a research scientist to support research and development of cutting-edge formal methods applied to software systems. The research scientist will support a team that invents, prototypes, and evaluates new formal methods and software security approaches throughout the systems software stack. Some topics of interest to a good candidate may include: theorem provers (e.q., Rocq/Coq, Lean, Isabelle), SMT solvers, programming languages theory (e.g., operational semantics), functional programming, compilers (e.g., frontends, IR & optimization, backends), automated program analysis and software testing. Interest in systems software (e.g., operating systems including RTOS, hypervisors), computer architecture (e.g., tagged architectures), and peripheral hardware (e.g., custom device drivers, FPGA hardware, bus protocols) is a plus. Secure and Resilient Systems research scientists need a strong background in computer science fundamentals (e.g., algorithms, data structures, theory of computation, programming languages), experience with software development practices for large projects (e.g., version control, debugging techniques), an understanding of the system software stack and the software/hardware interface (e.g., at least one ISA, assembly code), and propensity for the research process (e.g., breaking big problems down, designing experiments, analyzing data). If you have taken programming languages theory, formal methods, compilers, computer architecture and/or operating systems courses, you should apply for this position. If you have experience implementing and proving systems using a theorem prover such as Rocq/Coq or Lean, you definitely should apply for this position. If you have hacked on seL4, have proved the correctness of a crypto protocol implementation in Rust, or know the pros and cons of omnisemantics then you need to apply for this position!