Formal Verification & Proof Systems Engineer (Rocq / TLA+)

About the Role

We’re building a platform whose core value is trustworthy inference under explicit contracts: delay algebra, window validity, stability tests, and refuse-to-claim behavior when assumptions break. We already have strong mathematical models—now we want to harden them: make key claims machine-checkable, make invariants executable, and make pipeline/state behavior provably safe.

This role lives at the intersection of proof engineering (Rocq/Coq), spec engineering (TLA+), and proof-adjacent regression guardrails that run in CI. You turn “we believe this is true” into checked artifacts.

What You’ll Own

• Rocq (Coq) formalization of the delay calculus core: definitions, operators, composition rules, equivalences, key lemmas.
• Certificates / proof-carrying checks: machine-checkable receipts that validate outputs against stated assumptions (where feasible).
• TLA+ system specifications: model the runtime pipeline and failure modes (ingest → windowing → co-timing → gating → outputs), including concurrency/retries/ordering.
• Executable invariants: map contracts into tests/model checks/CI gates (property-based tests + formal checks).
• Math programming infrastructure: proof/code libraries and workflows so the team can extend foundations safely.

What You’ll Do

• Pick high-leverage targets to formalize: the pieces that, if wrong, create false trust.
• Formalize core semantics: delay operators, window semantics, commutation assumptions, stability criteria in Rocq.
• Prove key properties (or create proof-backed kernels): rewrite correctness, “valid window ⇒ allowed cancellation,” abstain safety properties.
• Model pipeline behavior in TLA+ with temporal properties like: “no report unless gates pass,” “every output has a receipt,” “retries don’t reorder truth.”
• Integrate proofs/spec checks into CI with a workflow that protects correctness without stalling engineering.
• Support algorithm and systems teams: translate derivations into formal statements; review foundation-touching changes.

Concrete Deliverables

• A Rocq library for delay calculus primitives (operators, composition, rewrite rules, equivalence relations).
• A set of machine-checked lemmas corresponding to core contract claims used by the product.
• A TLA+ spec suite for the runtime pipeline with model-checkable properties covering failure modes and concurrency edges.
• A proof-to-tests mapping: each formal claim paired with executable tests or runtime assertions where appropriate.
• A developer workflow: templates, conventions, and docs so others can contribute without breaking proofs.

Required Qualifications

• Strong experience with Rocq/Coq proof engineering: definitions, lemmas, tactics, structuring projects, maintaining proofs over time.
• Experience with formal specification tools (TLA+ preferred; Alloy/Lean/Isabelle acceptable if you can ramp to TLA+).
• Comfort with mathematical modeling: algebraic structures, semantics, and reasoning about exact vs approximate statements.
• Ability to collaborate with engineers: translate informal requirements into formal statements and back into actionable constraints.

Preferred Qualifications

• Background in signal processing/estimation/control or time-delay systems (helpful, not required).
• Experience with proof-adjacent production guardrails: certificates, verified kernels, formally specified APIs.
• CI hygiene for formal projects: build tooling, caching, proof performance.
• Experience writing specs for distributed systems (ordering, retries, idempotency, audit logs).

How You’ll Be Measured (First 60–90 Days)

• You stand up a minimal but real proof/spec backbone that runs in CI.
• You formalize and prove at least one high-leverage property that protects against false confidence.
• You produce a TLA+ spec that catches at least one subtle pipeline bug or ambiguity early.
• The team moves faster because invariants are explicit and regression-proofed.

Working Style

• You’re pragmatic: formalize the pieces that reduce real risk, not “prove the universe.”
• You like small trusted kernels and clear semantics.
• You believe correctness is a product feature—and you build tools that keep it that way.

Title & Level

Formal Verification & Proof Systems Engineer (Rocq / TLA+) (senior IC; can scale to Staff/Principal if owning the verification roadmap), partnering with applied math/DSP, backend, and validation teams.