Topics

One URL per cluster. The H1 is the question they typed.

Discovery pages, dated. Newest first in the log; here they sit with the day they shipped. If an existing section already owns the cluster, we edit that section instead of minting a twin.

28 Sep 2026 Solver latency clean A last VALID on realize specs/system/auth after four minutes is not a cheap proof. proof audit --check solver_latency_clean names the silent slice. Z3/Kind2 on one function is not that hop. Jama still authors.
28 Sep 2026 Trivial lemma A last PROVE on AddModel(a, b) == a + b can be a restatement of the model body. proof audit --check trivial_lemma names the silent lemma. Lemma branch coverage is not that hop. Jama still authors.
28 Sep 2026 Lemma branch coverage A last PROVE on the positive arm of Abs can leave the negative arm with an empty covered_by. proof audit --check lemma_branch_coverage names the silent lemma. Lemma binding freshness is not that hop. Jama still authors.
28 Sep 2026 Lemma binding freshness A separate-file lemma can keep its last PROVE after the bound function moved. proof audit --check lemma_binding_freshness names the silent binding. Formalization lemma verdict consistency is not that hop. Jama still authors.
28 Sep 2026 Formalization lemma verdict consistency A SYS-REQ can keep formalization_status: valid after the lemma cache is still timeout. proof audit --check formalization_lemma_verdict_consistency names the silent overstatement. Z3/Kind2 on one function is not that hop. Jama still authors.
28 Sep 2026 Approved guarantee KI conflict An approved guarantee can keep its stamp after an open known issue names the same id. proof audit --check approved_guarantee_ki_conflict names the silent approval. Approvals current is not that hop. Jama still authors.
28 Sep 2026 Contract alignment clean A cobra file can keep growing flags after the help topic never landed. proof audit --check contract_alignment_clean names the silent command. Design by contract is not that hop. Jama still authors.
28 Sep 2026 Assume contract consistency A host can keep // reqproof:assume ClearSession after the callee lost its lemma. proof audit --check assume_contract_consistency names the silent assume. Design by contract is not that hop. Jama still authors.
28 Sep 2026 Annotation validity A comment can still name SYS-REQ-9999 after the YAML is gone. proof audit --check annotation_validity names the silent ID. Autolink clean is not that hop. Jama still authors.
27 Sep 2026 Gaps clean An output can stay ? while Kind2 still prints realisable. proof audit --check gaps_clean names the silent unconstrained output. Variable drift is not that hop. Jama still authors.
27 Sep 2026 Circular deps clean Two files can parent each other while coverage still prints 100%. proof audit --check circular_deps_clean names the silent loop. Webpack imports are not that hop. Jama still authors.
27 Sep 2026 Role references resolve A role can name a renamed check, a deleted help topic, or a retired requirement while the playbook stays green. proof audit --check role_references_resolve names the silent drop. Empty-is-win language is not that hop. Jama still authors.
27 Sep 2026 Autolink clean A comment can name an unconfigured prefix and still vanish from the graph. proof audit --check autolink_clean names the silent drop. Zero annotations still pass. Jama still authors.
27 Sep 2026 Role prompt hygiene A role can prize an empty finding list, or cap findings per worker, while the sweep stays green. proof audit --check role_prompt_hygiene names the silent empty. A resource cap is not that hop. Jama still authors.
27 Sep 2026 Orphan code A production helper can ship with no Implements: line while coverage stays green. proof lint --check orphan_code_clean names the silent shrink. Dead code is not that hop. Jama still authors.
27 Sep 2026 Code signal deadline cast unreviewed An executeAfter row packed into uint32 can sit as cast noise with no packing campaign. proof audit --check code_signal_deadline_cast_unreviewed names the silent packing. CodeSignal is not that hop. Jama still authors.
27 Sep 2026 Code signal suppressions reviewed An http.* skip can sit with no reason, an expired date, and no path. proof audit --check code_signal_suppressions_reviewed names the silent exception. CodeSignal is not that hop. Jama still authors.
27 Sep 2026 Code signal obligations reviewed A SARIF hit can sit on FetchPolicy while the owner never listed the timeout class. proof audit --check code_signal_obligations_reviewed names the silent scanner. CodeSignal is not that hop. Jama still authors.
27 Sep 2026 Obligation witness grounded A coverage-trackable colon triple can sit on a tautological test that never runs the impl. proof audit --check obligation_witness_grounded names the silent theater. Jama still authors.
27 Sep 2026 Obligation profile evidence complete A class mapped to an evidence profile can sit with a colon triple and no passing result file. proof audit --check obligation_profile_evidence_complete names the silent triple. Jama still authors.
26 Sep 2026 Obligation suppression reviewer An error-severity suppress can sit with a long reason and no reviewed_by. proof audit --check obligation_suppression_reviewer names the silent unsigned skip. Jama still authors.
26 Sep 2026 Obligation suppression rationale A suppress can sit with reason TODO. proof audit --check obligation_suppression_rationale names the silent placeholder. Jama still authors.
26 Sep 2026 Obligation delegation resolves A delegated_to id can sit after the target dropped the class. proof audit --check obligation_delegation_resolves names the silent pointer. Jama still authors.
26 Sep 2026 Obligation decomposition complete A parent can list a class and the satisfying child never carries it. proof audit --check obligation_decomposition_complete names the silent drop. Jama still authors.
26 Sep 2026 Obligation baseline Tags can fire a catalog class with no accept and no suppress. proof audit --check obligation_baseline names the silent omission. Jama still authors.
26 Sep 2026 Obligation enforcement backed A cataloged checklist class can sit with no signal and no evidence. proof audit --check obligation_enforcement_backed names the silent no-op. Jama still authors.
26 Sep 2026 Acceptance witness quality An :acceptance tag can sit on a child unit test. proof audit --check acceptance_witness_quality names it. Jama still authors.
26 Sep 2026 Acceptance review current An AC list can sit on the STK with no stamp. proof audit --check spec_lint_acceptance_review_current names it. Jama still authors.
26 Sep 2026 Concern adjudicated An open YAML note can sit forever with no review_due. proof audit --check concern_adjudicated names it. Jama still authors.
26 Sep 2026 Problem reports reviewed A DEFECT can stamp covered while the hardening never landed. proof audit --check problem_reports_reviewed names it. Jama still authors.
26 Sep 2026 Change record lands A CHG can close with an affects list while no requirement cites it back. proof audit --check change_record_lands names it. Jama still authors.
26 Sep 2026 Approval motivation present A second stamp that still matches the shall looks current if the fingerprint did not change. proof audit --check approval_motivation_present names it. Jama still authors.
25 Sep 2026 Mirror stale A source edit that only duplicates a Verifies line still looks complete if the annotation cells did not move. proof audit --check mirror_stale names it. Jama still authors.
25 Sep 2026 Catalog semantic bindings reviewed A scan match that is neither bound nor rejected still looks reviewed if catalog completeness stayed green. proof audit --check catalog_semantic_bindings_reviewed names it. Jama still authors.
25 Sep 2026 Defect review current A spec with code links and no defect_review stamp still looks reviewed if no KnownIssue was filed yet. proof audit --check defect_review_current names it. Jama still authors.
25 Sep 2026 Severity inflation A critical stamp with no surface, no vector, and no risk basis still looks like disclosure-grade work. proof known-issue check names it. Jama still authors.
25 Sep 2026 CVSS severity consistent A low label on a still-critical CVSS vector drops the record out of every high-end hop. proof audit --check cvss_severity_consistent names it. Jama still authors.
25 Sep 2026 Security relevance consistent A security-named KnownIssue with cve_surface: none and no CVSS vector drops out of the security lens. proof audit --check security_relevance_consistent names it. Jama still authors.
25 Sep 2026 MC/DC ignore classified A green coverage cell on a bare ignore is bookkeeping, not a named exemption. proof audit --check mcdc_ignore_classified names it. Jama still authors.
25 Sep 2026 MC/DC known issue disposition stale A KI-gated exemption that outlives its fixed bug is a leftover lie. proof audit --check mcdc_known_issue_disposition_stale names it. Jama still authors.
25 Sep 2026 Known issue template transfer An open KnownIssue that names a class without listing isomorphic sites leaves the second sink untracked. proof audit --check known_issue_template_transfer names it. Jama still authors.
25 Sep 2026 Known issue sibling disposition A fixed KnownIssue that leaves open siblings or unmarked sites is a silent close. proof audit --check known_issue_sibling_disposition names it. Jama still authors.
25 Sep 2026 Known issue severity prose consistent A title that reads HIGH on a record filed low is a quiet downgrade. proof audit --check known_issue_severity_prose_consistent names it. Jama still authors.
25 Sep 2026 Known issue security remediation present A security-relevant KnownIssue with no remediation or mitigation is unnamed containment. proof audit --check known_issue_security_remediation_present names it. Jama still authors.
24 Sep 2026 Known issue recheck due A disclosed KnownIssue whose recheck date has lapsed is overdue. proof audit --check known_issue_recheck_due names it. Jama still authors.
24 Sep 2026 Deployment tvl verified A high claim with no TVL and no outside grade is unanchored. proof audit --check deployment_tvl_verified names it. Jama still authors.
24 Sep 2026 Submission validated A submitting KnownIssue with empty gates is not ready. proof audit --check submission_validated names it. Jama still authors.
24 Sep 2026 Poc quality checked A missing poc_quality block is not a review. proof audit --check poc_quality_checked names it. Jama still authors.
24 Sep 2026 Known issue poc quality effective A present but false poc_quality block is not a review. proof audit --check known_issue_poc_quality_effective names it. Jama still authors.
24 Sep 2026 Known issue mirror anchor relevant A declared mirror: whose resolved scope the KI never touches is off-scope. proof audit --check known_issue_mirror_anchor_relevant names it. Jama still authors.
24 Sep 2026 Known issue affected requirements present An empty affected_requirements list is invisible to the trace graph. proof audit --check known_issue_affected_requirements_present names a contract-less KI. Jama still authors.
24 Sep 2026 Known issue reproducer consistent An accept-verb test name is not the secure contract. proof audit --check known_issue_reproducer_consistent names a contradiction. Jama still authors.
24 Sep 2026 Known issue reproducer present and resolves Prose in reproduction_steps is not a runnable selector. proof audit --check known_issue_reproducer_present_and_resolves names a stale command. Jama still authors.
24 Sep 2026 High severity reproducer grade A CVSS high is not an executed witness. proof audit --check high_severity_reproducer_grade names a silent headline. Jama still authors.
24 Sep 2026 High severity obligation without vector A CVSS high is not a campaignized class. proof audit --check high_severity_obligation_without_vector names a silent hazard. Jama still authors.
24 Sep 2026 Vector campaign closure An ad campaign is not an opened hunt with an exit. proof audit --check vector_campaign_closure names a silent partial. Jama still authors.
23 Sep 2026 Obligation evidence complete A green checklist is not a triple. proof audit --check obligation_evidence_complete names a missing kind. Jama still authors.
23 Sep 2026 Code signal unbindable A CodeSignal interview is not a draft class. proof audit --check code_signal_unbindable names a silent proposal. Jama still authors.
23 Sep 2026 Vector campaign hygiene An ad campaign is not a hunt YAML. proof audit --check vector_campaign_hygiene names a dangling KI. Jama still authors.
23 Sep 2026 Unresearched P0 vectors A CodeSignal interview is not an opened hunt. proof audit --check unresearched_p0_vectors names a silent P0. Jama still authors.
23 Sep 2026 Known issue complete A Salesforce bulletin is not a failing test. proof audit --check known_issue_complete names a sticky note. Jama still authors.
23 Sep 2026 Data constraints complete A SQL CHECK is not a partition. proof audit --check data_constraints_complete names a gap or an overlap. Jama still authors.
23 Sep 2026 Catalog version pinned A Magento SKU is not a catalog pin. proof audit --check catalog_version_pinned names a pin that no longer matches. Jama still authors.
23 Sep 2026 Change evidence complete A Jira ticket is not a covering DEFECT. proof audit --check change_evidence_complete names a declared fix without backing. Jama still authors.
22 Sep 2026 Residual kill hygiene A spreadsheet kill is not a sample_table. proof audit --check residual_kill_hygiene names a closed kill without samples. Jama still authors.
22 Sep 2026 Approvals current A Slack stamp is not a current fingerprint. proof audit --check approvals_current names a stale shall. Jama still authors.
22 Sep 2026 Known issues reviewed A Salesforce bulletin is not a dated YAML. proof audit --check known_issues_reviewed names a stale review_date. Jama still authors.
22 Sep 2026 Waivers reviewed An empty expiry is not a review. proof audit --check waivers_reviewed names the expired skip. Jama still authors.
22 Sep 2026 Documented claim verified A Sphinx percent is not a named claim cell. proof audit --check documented_claim_verified warns when the cell is incomplete. Jama still authors.
16 Sep 2026 Variable drift A green gaps report is not list/sentence agreement. proof audit --check variable_drift names the requirement. Jama still authors.
16 Sep 2026 Vacuous requirements A green SAT is not a constraint. proof audit --check vacuity_clean names the vacuous or still-unchecked requirement. Jama still authors.
16 Sep 2026 Obligation completeness A green STK is not a covered checklist. proof audit --check obligation_completeness names the class with no SYS-REQ. Jama still authors.
16 Sep 2026 Verification chain A green parent is not a verified tree. proof gaps specs/system --check verification_chain names the child that never ran. Jama still authors.
16 Sep 2026 Orphan tests A green Test* is not evidence until it names a live requirement. proof lint --check orphan_tests_clean names the symbol. Jama still authors.
16 Sep 2026 Catalog completeness Four invariants on yaml, catalog, rules, and checklists. proof audit --check catalog_completeness fails the drift. Jama still authors.
16 Sep 2026 Software verification A green suite is not the graph pipeline. proof verify runs it. Jama still authors.
16 Sep 2026 Ambiguous requirements Two green shalls can still share a variable. proof audit --check ambiguity_reviewed names the pair. Jama still authors.
16 Sep 2026 Spec conformance A green formula is not a read of the Go. proof audit --check spec_lint_spec_conformance_review_grounded wants a citation. Jama still authors.
15 Sep 2026 Non functional requirements A green quality list is not a category table. proof status names the mix. Jama still authors.
15 Sep 2026 Software metrics A green DORA board is not spec-set health. proof gaps specs/system --check metrics names the pile. Jama still authors.
15 Sep 2026 Software checklist A green quality PDF is not a campaign stamp. proof audit --check process_checklist names the next eligible step. Jama still authors.
15 Sep 2026 Taint analysis A green sanitizer list is not a trust fact. proof audit --check trusted_outputs_from_untrusted_inputs reads trust: client. Direct edges only. Jama still authors.
15 Sep 2026 Test impact analysis A green full suite is not a named plan. proof test affected reads traces and Verifies rows. Incomplete evidence falls back to the full suite. Jama still authors.
14 Sep 2026 Requirement review A Slack walkthrough is not a brief. proof review req SYS-REQ-010 names traces, witnesses, and impact. It does not move status. Jama still authors.
14 Sep 2026 Requirements validation A silent drop is not valid. proof validate fails the unquoted colon. SEBoK still owns Boehm. Jama still authors.
13 Sep 2026 Requirements quality A green description is not quality. proof gaps specs/system --check quality fails empty FRETish. Jama still scores the programme. Jama still authors.
13 Sep 2026 Requirement lifecycle A Slack done is not review. proof req status SYS-REQ-010 --to review records the hop. BABOK still owns the knowledge area. Jama still authors.
13 Sep 2026 Stakeholder requirements A SYS-REQ import is not L0. proof audit --check stakeholder_requirements_exist fails when specs/stakeholder is empty. SEBoK still owns the workshop. Jama still authors.
13 Sep 2026 Coverage threshold A global 82% is not the changed shall. proof audit --check coverage_threshold judges each in-scope requirement against an imported profile. Vitest still owns the runner. Jama still authors.
13 Sep 2026 Equivalence partitioning A wiki of valid vs invalid is not a domain. proof verify-properties specs/system asks Z3 whether authored partitions cover the input without overlap. GeeksforGeeks still owns the glossary. Jama still authors.
13 Sep 2026 Slow tests A suite wall clock is not a named leaf. proof test slow lists cases whose body crossed the threshold. pytest-benchmark still owns the timer. Jama still authors.
13 Sep 2026 Documentation coverage A Sphinx percent is not a requirement doc. proof audit --check documentation_coverage inventories documented_by paths. Compodoc still owns the docstring bar. Jama still authors.
12 Sep 2026 Requirements assumptions A Slack “we assume the vendor is up” is not a boundary. proof req assumptions list inventories req_type=assumption with an owner and a review date. PMI still owns the project log. Jama still authors.
12 Sep 2026 Formal methods Three green fixtures are not a universal claim. proof verify-properties specs/system asks Z3 on authored variable properties. Coq still owns the assistant. Jama still authors. Proof does not infer the property.
12 Sep 2026 What is model checking, and how do I keep the traces true in CI? A lecture is not a verdict. proof realize specs/system autopilot --diagnose asks Kind2 on the Lustre contract. SPIN still owns Promela. Jama still authors. Proof does not implement the checker.
12 Sep 2026 Risk acceptance A Slack “we accept this” is not a signature. proof risk accept refuses a silent write without --accepted-by and --review-date. Metricstream still owns GRC. Jama still authors.
12 Sep 2026 Loop invariant A green walk of the slice is not establishment. proof verify-lemma --solver z3,cvc5 --tags reqproof_proof ./... refuses a silent pass when a for has no // reqproof:invariant, or when preservation is SAT. Dafny still owns the language. Jama still authors.
12 Sep 2026 Negative testing A green authorized request is not a reject. proof audit --check negative_path_witness_required refuses a silent pass when a security-classed shall has only a happy-path test. go test still runs the case. Jama still authors.
12 Sep 2026 Integration testing Green children are not the wired boundary. proof audit --check integration_evidence_witnessed refuses a silent pass when an INT-REQ has only unit tests. Testcontainers still runs the stack. Jama still authors.
12 Sep 2026 Fuzz testing Invalid inputs are the fuzzer's job. A :fuzz triple on a Test* function is not. proof audit --check fuzz_evidence_carrier_valid refuses annotation-only credit. go test -fuzz still mutates. Jama still authors.
12 Sep 2026 Acceptance criteria A Done list on a user story is not an acceptance test. proof audit --check acceptance_criteria_witnessed refuses a silent pass when a child's unit tests stand in for the assembled whole. Jira still owns the story. Jama still authors.
12 Sep 2026 Software problem report Class-closure after the fix, not a Done ticket. proof problem-report validate refuses a closed stamp without hardening. Jira still owns the tracker. Jama still authors.
12 Sep 2026 Pull request review The requirement blast radius on this branch, not LGTM on the Go. proof review-pr lists changed shalls, approval drift, and files to inspect. GitHub still owns the thread. Jama still authors.
11 Sep 2026 System requirements review The NASA first gate from this graph this commit, not last month's SRR pack. proof gate srr assesses existence, validation, levels, draft status, and blocking risks. Jama still authors.
11 Sep 2026 Critical design review The NASA detailed-design gate from this graph this commit, not last month's CDR pack. proof gate cdr assesses annotations, autolink, the build, and orphan code. Jama still authors.
11 Sep 2026 Test readiness review The NASA test gate from this graph this commit, not last month's TRR pack. proof gate trr assesses tests, coverage, MC/DC, fixtures, Z3, and suspect links. Jama still authors.
11 Sep 2026 Software verification report The completeness dump from this graph this commit, not last quarter's V&V PDF. proof doc generate verification-report prints the current checks. Jama still authors.
11 Sep 2026 Interface control document The INT-REQ that still matches both sides this commit, not a PDF from last quarter. proof audit --check interface_staleness_clean fails when the fingerprint drifted. Jama still authors.
11 Sep 2026 Requirements diagram The live SpecTree as Mermaid, not a SysML drawing from last quarter. proof diagram hierarchy --format mermaid prints the counts. Jama still authors.
11 Sep 2026 Requirements decomposition One parent shall split into owned software or interface children. proof req decompose previews the files; spec_lint_decomposition_adds_refinement fails a copy-paste child. Jama still authors.
11 Sep 2026 Inconsistent requirements Two shalls that cannot both hold. proof check consistency fails on UNSAT; consistency_pair_coverage fails when zero pairs were examined. Jama still authors.
11 Sep 2026 What is a software verification plan, and how do I keep it true in CI? Per-requirement strategies and expected evidence, before the code. proof verify-plan status --check fails when a planned item does not resolve. Jama still authors.
11 Sep 2026 What is requirements completeness, and how do I keep it true in CI? Declared classes, catalog entries, signal rules, and checklists. proof audit --check catalog_completeness fails when they disagree. Jama still authors.
11 Sep 2026 What is software change impact analysis, and how do I keep the blast radius true in CI? The blast radius of a change. proof trace impact prints the graph. Jama still authors. LDRA still wins at C CIA.
11 Sep 2026 What is ARP 4754A, and how do I keep the system requirements true in CI? SAE guidance for civil aircraft and systems. proof req import lands the allocation. Jama still authors. Proof does not run FHA or PSSA.
10 Sep 2026 What is SARIF, and how do I keep the findings true in CI? OASIS JSON for analyzer findings. proof signals import binds the row. Jama still authors. Proof is not a SARIF viewer.
10 Sep 2026 What is k-induction, and how do I keep the traces true in CI? Kind2's base-plus-step engine on a Lustre contract. proof realize asks Kind2. Jama still authors. Proof does not implement k-induction.
10 Sep 2026 What is design by contract, and how do I keep the contracts true in CI? Assume/guarantee at a component boundary. proof check integration names an unmatched assume. Jama still authors. Proof is not Eiffel.
10 Sep 2026 What is ASD-STE100, and how do I keep the prose true in CI? Simplified Technical English as a lint on the YAML. proof lint --check spec_lint_prose_ste100 names the hedge. Jama still authors. Proof is not an ASD trainer.
10 Sep 2026 What are derived requirements, and how do I keep them true in CI? A shall that was not in the stakeholder set, filed as a SYS-REQ. proof req derive writes the YAML and the satisfies link. Jama still authors. Proof does not invent architecture constraints.
10 Sep 2026 What is linear temporal logic, and how do I keep the traces true in CI? One formula, one finite boolean trace. proof simulate names the first false step. Jama still authors. Proof is not a model checker.
10 Sep 2026 What are decision tables, and how do I keep the cells true in CI? Finite inputs, one output per cell. proof check tables names a missing, duplicate, or drifting cell. Jama still authors. Proof is not a DMN engine.
10 Sep 2026 What is differential testing, and how do I keep the two implementations true in CI? Same input, two shims, compare the envelopes. proof differential fuzz hunts a disagreement, then proof audit --check differential_conformance replays the corpus. Jama still authors. Proof is not a hypervisor.
10 Sep 2026 What is a software accomplishment summary, and how do I keep it true in CI? The SAR pack from this graph, not last week's Word file. proof gate sar --output sas.html writes HTML. Jama still authors. Proof is not a certificate.
10 Sep 2026 What is property based testing, and how do I keep the fixtures true in CI? Fixtures from authored variable semantics, not from last week's seed. proof proptest writes JSON, then proof verify-properties is the SMT result. Jama still authors. Proof is not Hypothesis.
10 Sep 2026 What is a software baseline, and how do I keep it true in CI? A named freeze of the shalls at a gate. proof baseline create writes YAML and a git tag, then proof baseline diff lists IDs added, removed, or changed. Jama still authors. Proof is not a CM database.
9 Sep 2026 What is requirements based testing, and how do I keep the vectors true in CI? Cases from the compiled shall, not from last week's suite. proof testgen writes JSON vectors, then the audit fails the merge when fixtures are stale. Jama still authors. Proof is not a test runner.
9 Sep 2026 What is ReqIF, and how do I keep the interchange true in CI? The OMG XML for exchanging requirements. proof req import --format reqif writes each SPEC-OBJECT as YAML in the graph. Jama still authors. Proof is not a ReqIF editor.
9 Sep 2026 What is the INCOSE Guide for Writing Requirements, and how do I keep the shalls true in CI? The shall-writing rules. proof validate --preflight accepts the sentence or it does not, then the audit fails the merge when the graph is stale. Jama still authors. Proof is not INCOSE membership.
9 Sep 2026 What is a requirements summary, and how do I keep it true in CI? Counts, IDs, and trace ratios from the current graph. proof doc generate req-summary prints the table, then the audit fails the merge when the graph is stale. Jama still authors. Proof is not an SRS.
9 Sep 2026 What is EN 50128, and how do I keep railway software true in CI? CENELEC railway control and protection software. proof realize runs Kind2 on the shalls, then the audit fails the merge when the graph is stale. A notified body keeps the certificate. Proof is not a SIL.
9 Sep 2026 What is DO-278, and how do I keep CNS/ATM software true in CI? Ground CNS/ATM software. proof mcdc measure ./... --engine go measures the Go you ship. VectorCAST still owns qualified C. Proof is not DO-330.
9 Sep 2026 What is a preliminary design review, and how do I keep it true in CI? A NASA lifecycle gate. proof gate pdr assesses SDD generation, interfaces, architecture, and circular deps, then fails the merge when a criterion is not ready. Jama still authors. Proof is not the review board.
9 Sep 2026 What is a software requirements specification, and how do I keep it true in CI? The shalls printed from the current graph. proof doc generate npr7150-srs renders purpose, specific requirements, and traces, then the audit fails the merge when the graph is stale. Jama still authors. Proof is not a Word template.
9 Sep 2026 What is a software design document, and how do I keep it true in CI? Architecture and unit design printed from the current graph. proof doc generate sdd renders components, interfaces, and traces, then the audit fails the merge when the graph is stale. Jama still authors. Proof is not a PDR.
9 Sep 2026 What is NASA-STD-8739.8, and how do I keep the software assurance evidence true in CI? Software assurance, software safety, and IV&V. proof doc generate verification-report prints the current rows, then the audit fails the merge when the graph is stale. OSMA keeps independence. Proof is not Fairmont.
9 Sep 2026 What is IEC 61508, and how do I keep the software safety requirements true in CI? Industrial functional safety. Part 3 is software. proof realize runs Kind2 on the shalls, then the audit fails the merge when the graph is stale. A TÜV assessment keeps the certificate. Proof is not a SIL.
9 Sep 2026 What is DO-333, and how do I keep formal analysis true in CI? Formal methods supplement to DO-178C. proof realize runs Kind2 on the shalls, then the audit fails the merge when the graph is stale. SPARK keeps FM.3. Proof is not DO-330.
8 Sep 2026 What is IEC 62304, and how do I keep the software design document true in CI? Medical software, Class A through C. Proof prints sdd from the current graph, then fails the merge when the graph is stale. A notified body keeps the certificate.
8 Sep 2026 What is ISO 26262, and how do I keep the software design document true in CI? Part 6 is software. Proof prints sdd from the current graph, then fails the merge when the graph is stale. VectorCAST keeps the qualified toolchain.
8 Sep 2026 How do I migrate from one language to another and guarantee the same behavior? Names can change. proof audit --check mirror_complete fails the merge when a ledger cell on the old language has no counterpart on the new one. Identical bytes are a different check.
8 Sep 2026 We ship features fast but I have no confidence they're correct. Who can independently verify that? Speed is not the missing instrument. proof audit --fail-level warn fails the merge when an approved shall has no witness. NASA IV&V keeps its job.
8 Sep 2026 How do I add a step so AI-written code can't ship if it violates a requirement? Make proof audit --fail-level warn a required check. The PR stays red when an approved shall has no witness. Keep GitHub and the comment bot.
4 Sep 2026 What is ISO 29148, and how do I keep the SRS hierarchy true in CI? ISO 29148 names four documents. Proof compiles SyRS and SRS, prints npr7150-srs from the current graph, and does not write a BRS.
4 Sep 2026 What is NPR 7150.2D, and how do I keep the SRS true in CI? NASA writes the procedure. Proof prints npr7150-srs from the current graph, then fails the merge when the graph is stale.
4 Sep 2026 What's the safest way to modernize legacy software that nobody fully understands? Do not invent the spec from the unread tree. Proof fails with proof audit --check mirror_complete when a ledger cell on the slice you keep vanished.
4 Sep 2026 We're migrating a critical service. How do I prove the new one matches the old one? Keep the canary. Proof fails with proof audit --check mirror_complete when a ledger cell on the old service has no counterpart on the new one.
3 Sep 2026 How do I let AI agents ship faster without shipping more bugs? Do not throttle the model. Proof fails the merge with proof audit --fail-level warn when the shall has no witness. Keep Cursor fast.
3 Sep 2026 What does a safe agentic development pipeline look like? The jobs you already run can all be green. Proof is the last job: proof audit --fail-level warn. Keep Actions, Sonar, and the merge queue.
3 Sep 2026 How do I keep correctness under control as AI accelerates our code output? The queue grew. The shall did not. Proof fails the merge with the same command at 3 PRs a day or 30. Keep Sonar and the review bot.
3 Sep 2026 How do I find the class of bugs my tests never check for? The suite is green on the inputs you wrote. Proof asks whether the shalls can be kept at all. Keep PITest and Hypothesis.
3 Sep 2026 Every release we fix bugs and new ones appear in the same area. How do we break the cycle? A closed ticket is one instance. Proof fails the merge when the area still has no shall with a witness. Keep Sentry and the quality gate.
3 Sep 2026 How do I know every requirement is actually covered by code and a test? Jama stores a filled cell. Proof fails the merge when an obligation has no annotated witness. Keep Jama and the cover report.
3 Sep 2026 How do I prove a database or API migration didn't change behavior? Flyway records that V42 applied. Proof fails the merge when a db_migration shall has no witness. Keep Flyway and Pact.
3 Sep 2026 We do SOC2 and pentests but nothing verifies the business logic is right. What fills that gap? A Type II letter is last quarter. Proof fails the merge when the shall has no witness. Keep the auditor and the pentest.
3 Sep 2026 What's the best way to review AI-generated code for correctness at scale? A review queue grows with every agent. Proof fails the merge when the shall has no witness. CodeRabbit still comments on the diff.
3 Sep 2026 My AI coding agent keeps producing plausible but wrong code. How do I catch that? The patch reads as if a person wrote it. Proof fails the merge when the shall has no witness. CodeRabbit still reviews the diff.
2 Sep 2026 Our tests pass but bugs still ship to production. Why, and how do I fix that? A green suite is a sample. Proof fails the merge when the shall has no witness. Sentry still files the ticket.
2 Sep 2026 How do I turn a written spec into obligations I can check against the code? A PDF shall is not an obligation. validate --preflight compiles it. TLA+ and Dafny still win at arbitrary specs.
2 Sep 2026 How do I connect a formal specification to my actual source code? The lemma sits on the function. implemented_by names it. Dafny and SPARK still win when the spec is the language.
2 Sep 2026 Is there a service that does formal verification of a component for me? Proof hangs Z3 lemmas on the functions you ship. TrustInSoft still wins on C. A Coq shop still wins on a kernel.
2 Sep 2026 What does a continuous correctness check in CI look like? The same proof audit, on every push, with --fail-level warn. A quarterly PDF is a date.
2 Sep 2026 AI generates our specs and our code. Who verifies the intent is right? A spec written from the code restates the code. An owner signs the shall. proof audit then fails the merge.
2 Sep 2026 How can I trust code generated by Claude or Copilot before merging it? Copilot and Claude write the patch. Proof fails the merge when the change has no witness.
2 Sep 2026 A customer reported a crash our whole test suite missed. How do I prevent that entire class? A green suite is a sample. Kind2 returns a counterexample for the class. Sentry still files the ticket.
2 Sep 2026 We're a fintech and need proof our transaction logic is correct. What are our options? PCI and SOC 2 do not read the shall. Proof fails the merge when the ledger row is missing.
2 Sep 2026 Who audits AI-generated code for correctness? Model-written code and model-written tests can agree. Proof holds both to a signed shall.
1 Sep 2026 How do I catch when an AI agent silently breaks an existing requirement? Reverse suspect: the code is newer than the shall. Diff review still reads the PR.
1 Sep 2026 How do I safely replace a legacy component that has no specs and no tests? Owners sign the shalls first. A golden master still pins bytes. Spec-from-code is circular.
1 Sep 2026 What guardrails should I put around autonomous coding agents? Proof fails the merge on a shall with no witness. Cursor rules still own the prompt.
1 Sep 2026 How do I make requirements executable so they're checked automatically? Proof fails the merge on a shall with no witness. Cucumber still owns Given-When-Then.
1 Sep 2026 What's the difference between test coverage and requirements coverage? A line report asks whether code ran. Proof asks whether an approved shall still has a witness.
1 Sep 2026 We passed a security audit but still ship functional bugs. What kind of audit catches those? A pentest and a SAST pass do not read the shall. Proof re-reads the code against the promise.
1 Sep 2026 How do I get an independent check that my software actually does what we promised customers? Proof re-reads one component against approved shalls. Crowdtesting and SOC 2 keep their jobs.
1 Sep 2026 How do I do hazard analysis for a software component and tie it to the code? Catalog class on the requirement. ACCEPT, SUPPRESS, DEFER, or DRAFT. Jama still authors the programme.
1 Sep 2026 How do I prove a specific function meets its specification using something like Z3 or Kind2? A Z3 lemma on the Go function. Kind2 on whether the shalls are implementable. SPARK keeps C.
1 Sep 2026 I need DO-178C style verification but I'm not in aerospace. What can I use? Proof re-runs the discipline in ordinary CI. LDRA keeps the qualified toolchain.
1 Sep 2026 How do I write FRETish requirements a compiler can check? Proof compiles FRETish, structured English, into temporal logic. TLA+, Alloy, and Dafny sit on this page.
1 Sep 2026 Proof vs LDRA LDRA measures C in a qualified toolchain. Proof measures the Go you ship. VectorCAST sits on this page.
31 Aug 2026 Proof vs Snyk A Snyk pass is a vuln scan. Proof is a requirement gate. Coverity sits on this page.
31 Aug 2026 Proof vs SonarQube A SonarQube quality gate is a ruleset on new code. Proof is a requirement gate. Semgrep sits on this page.
31 Aug 2026 Proof vs CodeRabbit CodeRabbit is an AI reviewer. Run it twice, the comments move. Proof is deterministic: a corpus you own, and findings with a reproducer.
31 Aug 2026 Proof vs Jama Connect Jama Connect stores asserted links. Proof re-reads the code. IBM DOORS sits on this page, not a twin.
31 Aug 2026 How do I rewrite a legacy system without introducing regressions? Characterization tests pin observed output. A Proof mirror pins the verification ledger the rewrite has to carry.
31 Aug 2026 Why do the same bugs keep coming back in our codebase? A recurring bug is an unpinned door. Quality gates notice it after it walks back in.
31 Aug 2026 What is a requirements traceability matrix, and how do I keep it true? DOORS and Jama store the links a human asserted. They never re-check that the code still keeps the requirement.
30 Aug 2026 How do I measure MC/DC coverage for my Go code? Statement coverage is not MC/DC. VectorCAST does not read Go. Proof does.
31 Aug 2026 How do I verify code that an AI agent wrote is actually correct? A green test written by the same agent is agreement, not correctness.