Skip to content

feat(prover): add whole-app React proof engine - #1471

Draft
aidenybai wants to merge 23 commits into
mainfrom
codex/react-proof-engine
Draft

feat(prover): add whole-app React proof engine#1471
aidenybai wants to merge 23 commits into
mainfrom
codex/react-proof-engine

Conversation

@aidenybai

@aidenybai aidenybai commented Jul 28, 2026

Copy link
Copy Markdown
Member

What this adds

This PR adds a private @react-doctor/prover package for whole-application React verification.

It builds a TypeScript program, extracts React Compiler HIR/CFG facts, constructs a versioned semantic graph, evaluates 36 React proof obligations, and independently checks the resulting certificate.

import { checkReactProofReport, proveReactApp } from "@react-doctor/prover";

const report = proveReactApp({ rootDirectory: "/path/to/app" });
const certificate = checkReactProofReport(report);

report.status; // "proved" | "refuted" | "incomplete"
certificate.status; // "valid" | "invalid"
  • proved: every discovered React unit satisfies every implemented obligation.
  • refuted: the prover found a concrete source-level counterexample.
  • incomplete: unsupported syntax, an opaque dependency, or an open runtime boundary prevented a proof.

incomplete is a failed proof, not a pass.

How it works

TypeScript project
  → React Compiler HIR/CFG snapshot
  → React semantic graph
  → per-component and per-Hook obligations
  → independent certificate checker
  → application verdict

The semantic graph records component calls, renders, Hooks, callbacks, execution phases, state transitions, effects, resources, ReactNode slots, context providers, Suspense/Error Boundaries, hydration roots, memo comparators, and their cross-file relationships.

The checker does not trust the analyzer's final verdict. It recomputes graph references, reciprocal links, topology sources, protocol equations, every obligation status, report totals, and the application verdict.

Proof contracts added

1. Hook order, ownership, and component invocation

Hooks must have a valid React owner and execute in the same order on every render. Components must be rendered by React rather than called as ordinary functions.

const Panel = ({ hidden }: { hidden: boolean }) => {
  if (hidden) return null;
  const [count] = useState(0); // refuted: conditional Hook
  return <output>{count}</output>;
};

Avatar({ name: "Ada" }); // refuted: direct component call

Claims: hook-order, hook-ownership, component-invocation, boundary-coverage.

2. Render purity, refs, and component identity

Render must be deterministic and must not mutate props, state, refs, or external state. Component identity must not be recreated in render.

const Clock = () => <time>{Date.now()}</time>; // refuted: non-idempotent render

const App = () => {
  const Item = () => <li>Item</li>; // refuted: unstable component identity
  return <Item />;
};

Claims: render-purity, ref-access, component-identity.

3. Effects, dependencies, cleanup, and scheduled work

The prover resolves captured reactive values, setup/cleanup alternatives, listener identity, timer handles, observer activations, and Strict Mode lifecycle repetition.

useEffect(() => {
  const onResize = () => setWidth(window.innerWidth);
  window.addEventListener("resize", onResize);
  return () => window.removeEventListener("resize", onResize);
}, []);

It refutes missing dependencies, mismatched listener identity/options, leaked timers or observers, render-time state cycles, and incomplete cleanup paths.

Claims: effect-dependencies, effect-cleanup, effect-state-updates, scheduled-callback-lifetime.

4. Async Effect ownership

Async completions must still belong to the Effect instance that writes their result.

useEffect(() => {
  let ignored = false;

  void loadUser(userId).then((user) => {
    if (!ignored) setUser(user);
  });

  return () => {
    ignored = true;
  };
}, [userId]);

Ungated post-await or Promise-chain writes are refuted because an older request can overwrite newer state.

Claim: async-effect-ownership.

5. Callback phases, Effect Events, and callable refs

Callbacks are tracked through local helpers, parameters, object properties, returns, JSX props, and synchronous higher-order calls. Each use is tied to its React phase.

const onTick = useEffectEvent(() => report(value));

useEffect(() => {
  const timer = setInterval(onTick, 1_000);
  return () => clearInterval(timer);
}, []);

Calling an Effect Event during render, exporting it, passing it to a child, or using a passively synchronized ref where commit freshness is required remains refuted or incomplete.

Claims: effect-event-usage, callable-ref-freshness.

6. Context and ReactNode topology

The prover distinguishes constructing a JSX value from actually rendering it. This prevents lexical JSX nesting from inventing provider, form, Suspense, Error Boundary, lifecycle, or hydration ancestry.

const Shell = ({ children }: { children: ReactNode }) => null;

<Shell>
  <Profile />
</Shell>; // Profile is constructed, but Shell never renders it

For effective renders, it follows direct children, named slots, aliases, fragments, portals, and project-local component edges while preserving provider/form/boundary frames.

Claims: context-topology, react-node-flow.

7. Reconciliation identity

List identity must follow the represented data rather than its current position.

items.map((item) => <Row key={item.id} item={item} />); // proved
items.map((item, index) => <Row key={index} item={item} />); // refuted when reorderable

Claim: reconciliation-identity.

8. Hook, reducer, and class state transitions

The prover resolves state/setter and reducer/dispatcher tuples, updater callbacks, execution roots, reducer totality, class lifecycle phases, direct mutations, and bounded update guards.

const [count, setCount] = useState(0);
setCount((previousCount) => previousCount + 1); // proved pure transition

const reducer = (state: State, action: Action): State =>
  action.type === "increment" ? { count: state.count + 1 } : state;

Direct this.state mutation, impure updater callbacks, render-time dispatch, escaped setters/dispatchers, partial reducers, and unguarded componentDidUpdate loops are rejected.

Claims: hook-state-transitions, reducer-purity, reducer-transitions, class-construction, class-state-transitions.

9. React 19 Actions, optimistic state, and forms

The graph models Transition Actions, Form Actions, Action State reducers, optimistic updates, and Form Status placement.

const [state, submitAction, isPending] = useActionState(saveProfile, initialState);

<form action={submitAction}>
  <ProfileFields />
  <SubmitButton />
</form>;

const SubmitButton = () => {
  const { pending } = useFormStatus();
  return <button disabled={pending}>Save</button>;
};

It checks that dispatches and optimistic writes occur inside modeled Actions, that Form Status has a real parent form, and that Transition work does not drive controlled inputs through an invalid deferred update.

Claims: transition-actions, form-actions, action-state, optimistic-state, form-status.

10. Imperative handles

The prover ties a useImperativeHandle factory to its ref, closed method set, dependencies, consumer binding, and invocation phase.

useImperativeHandle(
  ref,
  () => ({ focus: () => inputRef.current?.focus(), label: () => label }),
  [label],
);

Missing reactive dependencies, impure factories, open object spreads, shared refs, unresolved consumers, and stale methods do not receive a proof.

Claim: imperative-handle.

11. External stores

useSyncExternalStore requires symmetric subscription cleanup, stable snapshots, and server/client snapshot equivalence during hydration.

const value = useSyncExternalStore(
  (notify) => {
    listeners.add(notify);
    return () => listeners.delete(notify);
  },
  () => cachedSnapshot,
  () => serverSnapshot,
);

Fresh snapshot objects, missing cleanup, unresolved callback channels, and mismatched server snapshots are rejected.

Claim: external-store-consistency.

12. Lazy loading, Suspense, Error Boundaries, and use

The prover follows lazy renders and Promise resources through component, helper, Hook, and ReactNode-slot edges to their catching boundaries.

const Profile = lazy(() => import("./profile"));

<ErrorBoundary>
  <Suspense fallback={<Spinner />}>
    <Profile />
  </Suspense>
</ErrorBoundary>;

Lazy declarations must have stable identity and valid loaders. use(Promise) resources need stable cache identity, Suspense for pending state, and a valid Error Boundary for rejection.

Claims: lazy-suspense, error-boundary, use-resource.

13. Controlled host elements

Intrinsic inputs, textareas, and selects are checked for stable controlled ownership and exact synchronous updates.

const [name, setName] = useState("");

<input
  value={name}
  onChange={(event) => setName(event.currentTarget.value)}
/>;

Known controlled/uncontrolled switches, value plus defaultValue, absent/deferred/conditional writes, transformed values, and invalid file-input control are rejected.

Claim: host-control.

14. Hydration equivalence

Source-visible server and client roots must resolve to the same tree, environment behavior, and identifierPrefix.

const tree = <App />;

renderToString(tree, { identifierPrefix: "app-" });
hydrateRoot(document, tree, { identifierPrefix: "app-" });

The prover refutes browser-global first-render branches, host-default locale formatting, unequal prefixes, renderToStaticMarkup hydration, and hazards reached through children or custom Hooks. Framework-generated and dynamic roots remain incomplete.

Claim: hydration-equivalence.

15. React.memo bailout equivalence

Every path on which a custom comparator returns true must imply equality of every varying prop path observed by the component, including callbacks and nested values.

const Profile = memo(
  ({ name, revision }: Props) => <p>{name}: {revision}</p>,
  (previous, next) =>
    previous.name === next.name &&
    Object.is(previous.revision, next.revision),
);

The symbolic comparator model supports ===, !==, Object.is, &&, ||, !, conditionals, immutable aliases, and early-return guards. It refutes omitted props, callbacks, nested paths, rest props, unsafe disjunctions, and comparisons of shared prototype methods instead of their rendered receivers. Opaque helpers and dynamic reads remain incomplete.

Claims: memo-equivalence, memo-dependencies.

Certificate and schema

The independent checker rejects:

  • unsupported report or graph schemas;
  • duplicate IDs and dangling references;
  • invalid owner, callback, phase, and reciprocal links;
  • forged source/completeness flags;
  • protocol statuses that do not follow from their underlying facts;
  • missing or duplicate claim coverage;
  • report totals or application verdicts inconsistent with obligations;
  • removal of project-level evidence for unresolved proof boundaries.

This revision uses report schema 30 and semantic graph schema 36.

Corpus and validation

  • 36 proof claims
  • 416 checked-in TypeScript fixture projects
  • 660/660 static prover tests
  • 54/54 React 19.2.5 Chromium runtime oracles
  • 27/27 focused memo-equivalence tests
  • package typecheck, build, and built-package smoke passed
  • workspace tests, lint, typecheck, formatting, and JSON-report smoke passed
  • commit-range React Doctor scan: no issues
  • full GitHub CI and CodeQL: passed

Runtime oracles reproduce selected failures in real React, including stale memo output, hydration recovery, reconciliation state transfer, listener leaks, Strict Mode replay, stale async writes, Suspense/Error Boundary behavior, and controlled-input ownership. Runtime evidence calibrates fixtures but never upgrades an incomplete static proof.

Scope

This package remains private at 0.0.0. It does not change the React Doctor CLI, score, config, public JSON report, GitHub Action, or telemetry, so no Changeset is included.

A proved result covers the 36 implemented React contracts and the supported TypeScript/React subset. It does not prove application-specific business requirements, arbitrary third-party library behavior, framework-generated entrypoints, or unsupported syntax. Those remain explicit incomplete boundaries rather than implicit passes.

The research basis and per-contract soundness ledger are in packages/prover/research-log.md.

@pkg-pr-new

pkg-pr-new Bot commented Jul 28, 2026

Copy link
Copy Markdown

Open in StackBlitz

npm i https://pkg.pr.new/eslint-plugin-react-doctor@1471
npm i https://pkg.pr.new/oxlint-plugin-react-doctor@1471
npm i https://pkg.pr.new/react-doctor@1471

commit: f93a08c

@github-actions

github-actions Bot commented Jul 28, 2026

Copy link
Copy Markdown
Contributor

React Doctor found 254 new issues in 157 files · 46 errors & 208 warnings · score 43 / 100 (Critical) · 0 fixed · vs main

Errors

208 warnings

src/analyze-boundary-coverage.ts

  • ⚠️ L390 Array lookup inside a loop js-set-map-lookups

src/analyze-hydration-equivalence.ts

  • ⚠️ L73 Chained array iterations js-combine-iterations

src/build-react-semantic-graph.ts

  • ⚠️ L3300 Array lookup inside a loop js-set-map-lookups

src/check-react-proof-report.ts

  • ⚠️ L3030 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3817 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3826 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3890 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3893 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3937 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3940 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L3978 array.find() inside a loop js-index-maps
  • ⚠️ L3998 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L4001 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L4492 Chained array iterations js-combine-iterations

src/collect-effect-resource-protocols.ts

  • ⚠️ L333 Array lookup inside a loop js-set-map-lookups
  • ⚠️ L434 array.find() inside a loop js-index-maps
  • ⚠️ L471 array.find() inside a loop js-index-maps

src/collect-effect-scheduler-protocols.ts

  • ⚠️ L323 array.find() inside a loop js-index-maps

src/collect-external-store-protocol-variants.ts

  • ⚠️ L141 Chained array iterations js-combine-iterations

src/collect-host-control-protocols.ts

  • ⚠️ L96 Array lookup inside a loop js-set-map-lookups

src/collect-hydration-equivalence.ts

  • ⚠️ L432 Repeated property access in a loop js-cache-property-access

src/collect-reachable-functions.ts

  • ⚠️ L293 Array lookup inside a loop js-set-map-lookups

src/create-component-slot-flow.ts

  • ⚠️ L136 Repeated property access in a loop js-cache-property-access

src/get-canonical-react-api-name.ts

  • ⚠️ L41 Chained array iterations js-combine-iterations

src/is-component-prop-expression.ts

  • ⚠️ L16 Array lookup inside a loop js-set-map-lookups

src/utils/has-conditional-ancestor.ts

  • ⚠️ L22 Repeated property access in a loop js-cache-property-access

src/utils/is-effective-jsx-property-source.ts

  • ⚠️ L18 Array lookup inside a loop js-set-map-lookups

tests/fixtures/aliased-stale-effect/src/app.tsx

  • ⚠️ L1 Hook import alias disables hook lint checks hook-import-rename-loses-use-prefix
  • ⚠️ L10 Missing effect dependencies exhaustive-deps

tests/fixtures/async-effect-opaque-guard/src/app.tsx

  • ⚠️ L12 State update after await in an effect no-set-state-after-await-in-effect

tests/fixtures/async-effect-stale-write/src/app.tsx

  • ⚠️ L11 State update after await in an effect no-set-state-after-await-in-effect

tests/fixtures/callback-parameter-opaque-registration/src/app.tsx

  • ⚠️ L8 Pure function rebuilt every render prefer-module-scope-pure-function

tests/fixtures/class-impure-state-updater/src/app.tsx

  • ⚠️ L11 setState in componentDidMount no-did-mount-set-state

tests/fixtures/class-listener-capture-mismatch/src/app.tsx

  • ⚠️ L7 Class component acquires a resource with no teardown class-component-missing-component-will-unmount-teardown

tests/fixtures/class-listener-leak/src/app.tsx

  • ⚠️ L7 Class component acquires a resource with no teardown class-component-missing-component-will-unmount-teardown

tests/fixtures/class-update-loop/src/app.tsx

  • ⚠️ L11 setState in componentDidUpdate no-did-update-set-state

tests/fixtures/direct-component-call/src/app.tsx

  • ⚠️ L3 Component called as a function no-call-component-as-function

tests/fixtures/effect-event-dependency/src/app.tsx

  • ⚠️ L8 Missing effect dependencies exhaustive-deps

tests/fixtures/effect-event-shared-helper/src/app.tsx

  • ⚠️ L9 Missing effect dependencies exhaustive-deps

tests/fixtures/effect-self-cycle/src/app.tsx

  • ⚠️ L7 Effect updates its own dependency no-self-updating-effect

tests/fixtures/effect-state-update/src/app.tsx

  • ⚠️ L7 Effect updates its own dependency no-self-updating-effect
  • ⚠️ L7 setState reads a stale value rerender-functional-setstate

tests/fixtures/fresh-external-store-callback-prop-snapshot/src/app.tsx

  • ⚠️ L16 Pure function rebuilt every render prefer-module-scope-pure-function
  • ⚠️ L20 Pure function rebuilt every render prefer-module-scope-pure-function

tests/fixtures/helper-effect-state-update/src/app.tsx

  • ⚠️ L11 Missing effect dependencies exhaustive-deps

tests/fixtures/incomplete-class-custom-subscription-lookalike/src/app.tsx

  • ⚠️ L10 Class component acquires a resource with no teardown class-component-missing-component-will-unmount-teardown

tests/fixtures/incomplete-class-listener-method-reassigned/src/app.tsx

  • ⚠️ L7 Class component acquires a resource with no teardown class-component-missing-component-will-unmount-teardown

tests/fixtures/incomplete-class-opaque-state-updater/src/app.tsx

  • ⚠️ L11 setState in componentDidMount no-did-mount-set-state

tests/fixtures/incomplete-composed-form-action-submitter/src/app.tsx

  • ⚠️ L2 Pure function rebuilt every render prefer-module-scope-pure-function

tests/fixtures/incomplete-computed-event-prop-wrapper/src/app.tsx

  • ⚠️ L17 Pure function rebuilt every render prefer-module-scope-pure-function

158 more warnings not shown.

Reviewed by React Doctor for commit f93a08c. See inline comments for fixes.

@github-actions

github-actions Bot commented Jul 28, 2026

Copy link
Copy Markdown
Contributor

Interactive terminal E2E

React Doctor interactive terminal recording

Recorded from the built CLI at f93a08c in a real terminal. The fixture holds Git busy for three seconds, so Scanning... must appear immediately after project selection, then exercises the compact interactive report.

Download the GIF and MP4 artifact

@aidenybai aidenybai changed the title feat: add whole-app React proof engine prototype feat(prover): add whole-app React proof engine Jul 28, 2026
propFlow.phase === phase &&
propFlow.complete &&
propFlow.callbackIds.length > 0 &&
propFlow.callbackIds.every((callbackId) => callbackIds.includes(callbackId)),

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/js-set-map-lookups (warning)

This scales poorly because array.includes() inside a loop scans the whole list every time. Use a Set for constant-time lookups.

Fix → Use a Set or Map when you check for the same items over and over. Array.includes/find scans the whole list each time

Docs

);
}
if (hydration.status === ReactHydrationStatus.Unknown) {
const evidence = context.graph.hydrationRoots

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/js-combine-iterations (warning)

This loops over your list twice because .filter().map() makes two passes, so do it in one pass with .reduce() or a for...of loop

Fix → Combine .map().filter() style chains into one pass with .reduce() or a for...of loop, so you only loop over the list once

Docs

const observer = resourceSymbol ? constructorsBySymbol.get(resourceSymbol) : null;
if (observer?.kind !== resourceKind) continue;
observer.activationCalls.push(callExpression);
if (!observers.includes(observer)) observers.push(observer);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/js-set-map-lookups (warning)

This scales poorly because array.includes() inside a loop scans the whole list every time. Use a Set for constant-time lookups.

Fix → Use a Set or Map when you check for the same items over and over. Array.includes/find scans the whole list each time

Docs

if (!listener) continue;
const ownerFunction = getEnclosingFunction(registrationCall);
const reachableOwner = ownerFunction
? reachableFunctions.find(

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/js-index-maps (warning)

This gets slow as your list grows because array.find() runs inside a loop, so build a Map once before the loop for instant lookups

Fix → Build a Map once before the loop instead of calling array.find(...) inside it

Docs

if (!observerActivation) continue;
const ownerFunction = getEnclosingFunction(observerActivation);
const reachableOwner = ownerFunction
? reachableFunctions.find(

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/js-index-maps (warning)

This gets slow as your list grows because array.find() runs inside a loop, so build a Map once before the loop for instant lookups

Fix → Build a Map once before the loop instead of calling array.find(...) inside it

Docs


useEffect(() => {
invokeTick();
}, [invokeTick]);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/exhaustive-deps (warning)

invokeTick is rebuilt every render, so useEffect runs every time.

Fix → Don't blindly add missing dependencies. Read the hook callback first.

Bad:
useEffect(() => {
setCount(count + 1);
}, [count]);

Better:
useEffect(() => {
setCount((currentCount) => currentCount + 1);
}, []);

If the missing value is recreated every render, move it inside the hook or stabilize it before adding it to deps.

Docs


useEffect(() => {
invokeTick();
}, [invokeTick]);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/no-effect-with-fresh-deps (error)

Your useEffect runs every render because dep invokeTick is a new function built fresh each time, so === always fails.

Fix → Move the value inside the hook body and depend on its simple inputs instead, or wrap it in useMemo / useCallback so it stays the same between renders.

Docs

const [enabled, setEnabled] = useState(false);

useEffect(() => {
setEnabled(!enabled);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/no-self-updating-effect (warning)

setEnabled() updates enabled, which is also in this effect's dependency list. Guard the update or move the derivation out of the effect.

Fix → Break the loop: work the value out while rendering, set it in an event handler, or guard the update so it stops changing. See https://react.dev/learn/you-might-not-need-an-effect

Docs

const [count, setCount] = useState(0);

useEffect(() => {
setCount(count + 1);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/no-self-updating-effect (warning)

setCount() updates count, which is also in this effect's dependency list. Guard the update or move the derivation out of the effect.

Fix → Break the loop: work the value out while rendering, set it in an event handler, or guard the update so it stops changing. See https://react.dev/learn/you-might-not-need-an-effect

Docs

const [count, setCount] = useState(0);

useEffect(() => {
setCount(count + 1);

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

React Doctor · react-doctor/rerender-functional-setstate (warning)

You can lose this update because setCount(count + ...) reads a stale value.

Fix → Use the callback form: setState(prev => prev + 1) to always read the latest value

Docs

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant