Software Formal Methods Engineer

Sigil Logic builds AI for rigorous engineering. Our platform, HOARDE, is a multi-agent system that brings formal methods and model-based engineering into the workflows teams already use. It connects requirements, architecture, software, firmware, hardware, tests, and proofs; orchestrates the right verification tools for each problem; and produces an auditable record of why a system works.

We are building for teams whose systems must not fail. Our mission is to make high-assurance engineering practical and scalable: to turn decades of research and experience on nationally critical systems into an everyday engineering capability.

We believe formal methods are among the most powerful ways to make AI-generated systems trustworthy. We are working at the frontier where LLMs, automated reasoning, and real hardware and software meet, and we believe that combination will reshape how engineering is done.

We are expanding HOARDE's software formal-methods capabilities. We are looking for engineers who can move between code, specifications, verification tools, product infrastructure, and engineering evidence to make rigorous assurance part of software development.

You might prove properties of existing C, C++, or Rust code; recover a specification from code and documentation; build a compatible replacement; or construct new software from a machine-checkable model. The right method may be a contract, static analysis, symbolic execution, model checking, refinement, theorem proving, generated testing, or a combination of several.

A substantial part of the job is product development: turning formal-methods expertise into reliable integrations, agent workflows, analysis pipelines, and developer experiences. The rest applies those capabilities to demanding real systems, from embedded software and toolchains to libraries, services, and mixed hardware-software stacks. Project work exposes the gaps; the product turns each solution into a repeatable capability. We value sound technical choices and useful results more than allegiance to any one language or prover.

• Extend HOARDE's software-assurance capabilities through dependable tool integrations, machine interfaces, agent workflows, analysis pipelines, diagnostics, and evidence.
• Specify and verify real software, working from requirements, standards, code, tests, and operational behavior to define what correctness means.
• Select and combine appropriate techniques, including contracts, static analysis, symbolic execution, model checking, SAT/SMT-backed reasoning, refinement, theorem proving, fuzzing, and generated testing.
• Connect executable or mathematical specifications to source, intermediate representations, or binaries, making every claim and assumption precise.
• Work with existing and sometimes difficult codebases while preserving compatibility, performance, deployability, and maintainability alongside formal guarantees.
• Put verification and traceability into normal development workflows so specifications, proofs, tests, assumptions, and evidence evolve with the software.
• Turn successful project work into reusable product capabilities, verified software, and assurance artifacts that customers and other engineers can use.

• Hands-on experience applying formal verification, program analysis, or automated reasoning to real software, with an understanding of where your methods do and do not fit.
• Strong software-engineering fundamentals, practical depth in one systems or implementation language, and enough Kotlin/JVM experience to contribute to HOARDE's production codebase. You can read unfamiliar code and diagnose failures across tool boundaries.
• Experience with multiple verification approaches, or sufficient depth with one to demonstrate that you can learn adjacent methods quickly.
• A record of delivering usable tools, production software, or verified outcomes that others could run, maintain, or build upon — and a product mindset about reliability, usability, and repeatability.
• The ability to turn an informal claim into a precise specification, property, experiment, or assurance argument and explain what was and was not established.
• Clear communication, sound judgment about rigor and scope, self-direction in a small distributed team, and curiosity about making AI-generated software demonstrably trustworthy.

This role touches many tools and domains. Depth in any subset can be valuable.

• Languages and systems: Kotlin/JVM, C, C++, Rust, Python, compilers and intermediate representations, operating systems, runtimes, libraries, or networked systems
• Program analysis and model checking: CBMC, Frama-C, Crux, KLEE, abstract interpretation, symbolic execution, SAT/SMT solvers, or comparable techniques
• Specifications and implementation proofs: Cryptol, SAW, ACSL, SPARK, Dafny, Why3, refinement or equivalence proofs, or verified compilation
• Rust assurance: Kani, Verus, MIR-based analysis, unsafe-code reasoning, or proof-oriented Rust development
• Theorem proving and formal modeling: Lean, Rocq, Isabelle/HOL, PVS, ACL2, TLA+, Alloy, or another reasoning environment
• Product and workflow integration: Developer tools, stable machine interfaces, CI/CD/CV, reproducible proofs, actionable diagnostics, specification recovery, or reusable conformance suites

If the work sounds like you and you bring strong foundations in software engineering and formal methods, relevant applied work, and the ability to learn, we want to hear from you.

Sigil Logic is a small, early team. You will work directly with people who have spent their careers building high-assurance systems, and you will have real influence over our product, methodology, and engineering culture. We value intellectual range, precise communication, practical output, and colleagues who teach what they know while learning from others.

We are headquartered in Portland, Oregon, and work as a fully distributed organization. Being in Portland is welcome, but we will not let geography keep us from the right person.

Email join@sigillogic.com with your resume or CV and a short note about the software or formal-methods work you are proudest of. Links to code, papers, talks, or project artifacts are welcome but not required.

Learn more about Sigil Logic and HOARDE.