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.

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.