by eurekascience CORRECTNESS IN SCIENTIFIC COMPUTING The contributions
LOADING EUREKA

EUREKA FOR SCIENTIFIC COMPUTING

Correctness in
scientific computing.

Formal reasoning for the algorithms and software behind scientific results.

Modular.End-to-end.Machine-checked.

FOLLOW THE WORK

THE RESEARCH DIRECTION

Correctness alongside
performance.

Connecting scientific specifications to implementations through modular, end-to-end, machine-checked reasoning. With AI and Lean.

The NSF/DOE CS² program

THE INITIATIVE

THE CONTRIBUTION RECORD

Evidence from scientific software.

Reported issues, proposed patches, and upstream merges.

MOOSE / PHASE-FIELD KERNELS

Four findings. One proposed fix.

MOOSE powers multiphysics simulations, including nuclear-fuel modeling in BISON. These four kernel errors were found through Lean formalization.

  1. 01

    ACInterfaceKobayashi2

    A mobility derivative was missing from the diagonal Jacobian.

  2. 02

    CHInterfaceBase

    The coupled-gradient sum used the wrong variable index.

  3. 03

    ADACBarrierFunction

    An accumulator carried values between order parameters instead of resetting.

  4. 04

    ACInterface

    An off-diagonal Jacobian used the derivative for the kernel variable.

Issue #34180 Fix PR #34326

PETSc / NUMERICAL COMPUTING

Correctness, across the stack.

View on GitLab

PETSc provides parallel solvers, time integration, and optimization for large-scale scientific simulations.

UPSTREAM STATUS
PETSc issue reports, linked merge requests, upstream merge status, and dates.
StatusFindingSourceTimeline

SCIENCE IS A SHARED EFFORT

Thank you, contributors.