Formal Methods Engineer

About Sigil Logic

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.

The Role

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.

Core Responsibilities

• 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.

What We Require

• 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.