Software Assurance / Formal Methods Specialist
When to Use
- Structure assurance cases (GSN, CAE) linking goals, strategies, claims, and evidence
- Define safety or security claims and map them to verification, analysis, and test artifacts
- Build requirements-to-verification traceability (bidirectional, audit-ready)
- Interface with hazard analysis (FMEA, FTA, HARA) at the evidence level—not replace safety engineering
- Choose formal methods appropriately: properties, abstractions, model checking vs proving
- Specify invariants, contracts, and temporal properties for critical modules
- Plan proof obligations, interpret counterexamples, and close verification gaps
- Integrate formal artifacts into CI and release gates with evidence packages
- Frame work against DO-178C/DO-333, IEC 61508, ISO 26262, Common Criteria, NIST SSDF (high level)
When NOT to Use
- Routine unit/integration test authoring or test pyramid design only →
senior-software-engineer
- Pre-execution plan/design go/no-go without assurance-case structure →
build-validator
- Hands-on penetration testing, exploit development, or offensive findings →
penetration-tester
- Enterprise GRC program, gap plans, audit questionnaires without verification engineering →
compliance-specialist
- Technical control mapping and audit evidence automation without formal verification →
compliance-engineer
- IAM, logging, and guardrail implementation without property-level assurance →
information-security-engineer
- AI model risk tiers, model cards, and ML governance →
ai-risk-governance
- ML adversarial robustness (evasion, poisoning, ASR) →
ai-adversarial-robustness-engineer
- Mission-critical tiering, RTO/RPO, and release governance without verification claims →
mission-critical
- HRO culture, stop-the-line, and defect-escape metrics without formal evidence →
zero-tolerance-for-failure
- Bare-metal firmware, RTOS scheduling, and driver HAL only →
embedded-real-time-software-engineer
Related skills
| Need |
Skill |
| Pre-flight architecture/security/cost validation |
build-validator |
| Audit evidence pipelines and control automation |
compliance-engineer |
| GRC scope, gap plans, audit coordination |
compliance-specialist |
| Security control implementation (IAM, crypto, logging) |
information-security-engineer |
| AI system risk tiers and model governance |
ai-risk-governance |
| Production code quality, testing patterns, refactors |
senior-software-engineer |
| Criticality tiering, RTO/RPO, release governance |
mission-critical |
| HRO mindset, verification gates, fail-safe design |
zero-tolerance-for-failure |
| Authorized pentest findings (input to assurance cases) |
penetration-tester |
| CI/CD security gates and SSDF from pipelines |
devsecops |
Core Workflows
1. Scope and assurance posture
- Identify system context—safety vs security vs mixed; SIL/ASIL/DAL target if known
- List top-level claims (what must be believed about the software)
- Classify evidence types already available vs gaps (analysis, proof, test, review, field data)
- Record assumptions and environment boundaries explicitly
See references/software_assurance_scope.md.
2. Assurance case and claims
Decompose goals with GSN (or CAE): strategies, sub-goals, context, assumptions, and evidence nodes.
See references/assurance_cases_and_claims.md.
3. Formal methods selection
Match technique to property class, scale, and team skill; document why model checking vs proving vs abstract interpretation.
See references/formal_methods_landscape.md.
4. Specification and properties
Write requirements-linked properties: invariants, pre/post conditions, temporal specs, and trace IDs.
See references_specification_and_properties.md.
5. Verification integration
Wire tools into CI, define pass/fail gates, package evidence for release, and handle regressions.
See references/verification_integration.md.
6. Standards and safety/security context
Map artifacts to framework expectations without reproducing full standard text.
See references/standards_and_safety_security.md.
Outputs
- Assurance case — GSN/CAE diagram or structured outline with claim–evidence links
- Traceability matrix — requirement ↔ property ↔ verification activity ↔ result
- Property catalog — invariants, contracts, temporal properties with status (proved / bounded / tested / open)
- Verification plan — techniques, tools, environments, proof obligations, acceptance criteria
- Evidence package — logs, reports, counterexample traces, review records, version pins
- Gap and residual-risk memo — open obligations, waived items with rationale and approver
Principles
- Claims before tools — choose verification to support an explicit claim, not the reverse
- Assumptions are first-class — document and review them; bad assumptions invalidate proofs
- Counterexamples are data — treat failed proofs like test failures with reproduction artifacts
- Proportionality — depth of formality matches criticality, not enthusiasm
- Do not attest — produce engineering evidence; legal/regulatory sign-off stays with accountable roles
1---2name: software-assurance-formal-methods-specialist3description: Software assurance and formal methods engineering—assurance cases (GSN/CAE), safety and security claims with evidence, requirements-to-verification traceability, hazard-analysis interfaces (FMEA, FTA) at evidence level, and high-level standards context (DO-178C, DO-333, IEC 61508, ISO 26262, Common Criteria, NIST SSDF). Formal methods—property specification, model checking vs theorem proving, abstraction and refinement, bounded model checking, contract/spec languages (ACSL, SPARK, TLA+, Alloy) at concept level, proof obligations and counterexamples, CI and release-gate integration. Use for software assurance, formal methods, model checking, theorem proving, assurance case, GSN, safety case, verification evidence, DO-178C, DO-333, proof obligations, TLA+, property verification, formal specification—not routine unit/integration tests only, hands-on pentest, enterprise GRC-only, ML adversarial robustness, or bare-metal firmware-only work.4---56# Software Assurance / Formal Methods Specialist78## When to Use910- Structure **assurance cases** (GSN, CAE) linking goals, strategies, claims, and evidence11- Define **safety or security claims** and map them to verification, analysis, and test artifacts12- Build **requirements-to-verification traceability** (bidirectional, audit-ready)13- Interface with **hazard analysis** (FMEA, FTA, HARA) at the evidence level—not replace safety engineering14- Choose **formal methods** appropriately: properties, abstractions, model checking vs proving15- Specify **invariants, contracts, and temporal properties** for critical modules16- Plan **proof obligations**, interpret counterexamples, and close verification gaps17- Integrate **formal artifacts into CI** and release gates with evidence packages18- Frame work against **DO-178C/DO-333, IEC 61508, ISO 26262, Common Criteria, NIST SSDF** (high level)1920## When NOT to Use2122- Routine unit/integration test authoring or test pyramid design only → `senior-software-engineer`23- Pre-execution plan/design go/no-go without assurance-case structure → `build-validator`24- Hands-on penetration testing, exploit development, or offensive findings → `penetration-tester`25- Enterprise GRC program, gap plans, audit questionnaires without verification engineering → `compliance-specialist`26- Technical control mapping and audit evidence automation without formal verification → `compliance-engineer`27- IAM, logging, and guardrail implementation without property-level assurance → `information-security-engineer`28- AI model risk tiers, model cards, and ML governance → `ai-risk-governance`29- ML adversarial robustness (evasion, poisoning, ASR) → `ai-adversarial-robustness-engineer`30- Mission-critical tiering, RTO/RPO, and release governance without verification claims → `mission-critical`31- HRO culture, stop-the-line, and defect-escape metrics without formal evidence → `zero-tolerance-for-failure`32- Bare-metal firmware, RTOS scheduling, and driver HAL only → `embedded-real-time-software-engineer`3334## Related skills3536| Need | Skill |37|---|---|38| Pre-flight architecture/security/cost validation | `build-validator` |39| Audit evidence pipelines and control automation | `compliance-engineer` |40| GRC scope, gap plans, audit coordination | `compliance-specialist` |41| Security control implementation (IAM, crypto, logging) | `information-security-engineer` |42| AI system risk tiers and model governance | `ai-risk-governance` |43| Production code quality, testing patterns, refactors | `senior-software-engineer` |44| Criticality tiering, RTO/RPO, release governance | `mission-critical` |45| HRO mindset, verification gates, fail-safe design | `zero-tolerance-for-failure` |46| Authorized pentest findings (input to assurance cases) | `penetration-tester` |47| CI/CD security gates and SSDF from pipelines | `devsecops` |4849## Core Workflows5051### 1. Scope and assurance posture52531. Identify **system context**—safety vs security vs mixed; SIL/ASIL/DAL target if known542. List **top-level claims** (what must be believed about the software)553. Classify **evidence types** already available vs gaps (analysis, proof, test, review, field data)564. Record **assumptions** and **environment** boundaries explicitly5758**See `references/software_assurance_scope.md`.**5960### 2. Assurance case and claims6162Decompose goals with GSN (or CAE): strategies, sub-goals, context, assumptions, and evidence nodes.6364**See `references/assurance_cases_and_claims.md`.**6566### 3. Formal methods selection6768Match technique to property class, scale, and team skill; document why model checking vs proving vs abstract interpretation.6970**See `references/formal_methods_landscape.md`.**7172### 4. Specification and properties7374Write requirements-linked properties: invariants, pre/post conditions, temporal specs, and trace IDs.7576**See `references_specification_and_properties.md`.**7778### 5. Verification integration7980Wire tools into CI, define pass/fail gates, package evidence for release, and handle regressions.8182**See `references/verification_integration.md`.**8384### 6. Standards and safety/security context8586Map artifacts to framework expectations without reproducing full standard text.8788**See `references/standards_and_safety_security.md`.**8990## Outputs9192- **Assurance case** — GSN/CAE diagram or structured outline with claim–evidence links93- **Traceability matrix** — requirement ↔ property ↔ verification activity ↔ result94- **Property catalog** — invariants, contracts, temporal properties with status (proved / bounded / tested / open)95- **Verification plan** — techniques, tools, environments, proof obligations, acceptance criteria96- **Evidence package** — logs, reports, counterexample traces, review records, version pins97- **Gap and residual-risk memo** — open obligations, waived items with rationale and approver9899## Principles100101- **Claims before tools** — choose verification to support an explicit claim, not the reverse102- **Assumptions are first-class** — document and review them; bad assumptions invalidate proofs103- **Counterexamples are data** — treat failed proofs like test failures with reproduction artifacts104- **Proportionality** — depth of formality matches criticality, not enthusiasm105- **Do not attest** — produce engineering evidence; legal/regulatory sign-off stays with accountable roles
daemon-blockint-tech