Simproof

• 

• 

• 

• 

• 

Inspiration

AI can generate a convincing STEM animation while getting the physics subtly wrong. A degree/radian mix-up still draws a smooth projectile arc. A coarse numerical method can leak energy while the pendulum looks fine. Unlike a wrong worksheet answer a teacher can eyeball, a wrong simulation looks right, so the error reaches students unnoticed.

Teachers are already using AI to build lesson material, and prompt-to-simulation tools are appearing, but nothing checks the physics before a class sees it. Teachers should not have to inspect generated source code or trust a green badge supplied by the same model that wrote it. I built SimProof to put an independent correctness check between generation and publication, so a teacher can use AI for a custom lesson without gambling on whether the science is right.

What it does

Teachers already generate lesson material with AI, and AI simulation generators exist. Trusted libraries like PhET and Gizmos are excellent but fixed, so the moment a teacher needs a lesson outside them they turn to generation, where nothing checks whether the physics is right. Tools that generate a simulation from a prompt stay silent on correctness. SimProof is the correctness gate for that case: it generates a simulation and then proves it against an independent, reviewed physics policy before a teacher can publish it. Projectile motion and simple pendulum are the two domains whose verifier packs are reviewed and shipped today; they prove the gate works rather than define the audience.

A teacher describes a supported lesson in plain language. GPT-5.6 compiles that request into a strict concept specification with bounded parameters. Codex writes a pure simulation core and a thin renderer adapter in a disposable workspace.

The generated core never runs in the browser or application server. SimProof sends it to a network-disabled, unprivileged runner, collects normalized output, and checks that output with a reviewed application-owned domain pack. The verifier owns the equations, physical invariants, valid ranges, samples, and tolerances. A model cannot rewrite those rules to make its own artifact pass.

If a candidate fails, the report names the exact finding, GPT-5.6 explains the physics error in plain language as commentary that cannot change the verdict, and Codex may repair only the candidate files. A bounded run stops after its configured attempt cap. Only an exact artifact with current passing evidence can receive a Verified badge or be published. Changing the artifact or its governing dependencies makes the evidence stale.

Teachers can inspect the tested range, assumptions, policy version, tolerances, and artifact identity. Every visual simulation also has a keyboard-operable data view. Bundled verified examples work without provider credentials, and SimProof stores no student accounts or student records.

How I built it

The first version was a small Python proof. I wrote realistic negative controls for common projectile and pendulum mistakes, then confirmed that known-correct controls passed while the wrong implementations were rejected. That proof remains in the repository as independent evidence.

The product is a TypeScript monorepo with separate contracts, domain verifiers, provider adapters, persistence, web UI, and runner protocol packages. Shared Zod schemas validate every process boundary. SQLite stores lifecycle metadata, while a content-addressed artifact store binds reports to exact bytes.

GPT-5.6 and Codex do different jobs at runtime. GPT-5.6 maps the teacher's request to a schema-constrained ConceptSpec. Codex writes and repairs candidate artifacts. Neither defines scientific truth. The orchestrator owns attempts, cancellation, budgets, provenance, and persistence, but contains no domain equations.

I also used Codex to build the repository itself. First I wrote the product spec and twelve numbered plans, plus five ADRs for the decisions that set the trust model. Then I handed those plans to one long Codex session run by /goal and let it work through them in order. Every plan was a checkpoint with the same standing rule: write the failing tests first, build the plan, run an independent review pass, fix the findings, run pnpm check and the Python proof, and commit to main before moving on. Anything that changed the web app also got a browser smoke test. SESSION.md is the journal of that run, with each checkpoint's commit, tests, and resolved review findings. Almost the whole product came out of that single session. The pieces I added later, like the plain-language failure explanation, followed the same test-first discipline.

Challenges

The hardest part was deciding what the model must not own. An early design let a model produce an executable answer key. That creates a circular trust problem: the generator could make the verifier agree with the same mistake. The production design keeps equations, reference samples, invariants, and tolerance policy in reviewed domain packs. Models can select a supported concept and write a candidate, but cannot move the goalposts.

Generated code is hostile input even when its output looks plausible. The runner has a read-only root filesystem, no network, no secrets, no repository or persistent-data mount, dropped capabilities, bounded output, and forced cleanup. The application fails closed when that isolation is unavailable.

Verification language was another challenge. "Verified" cannot mean universally correct. In SimProof it means one artifact hash passed one named policy version over a recorded parameter space and tolerance set. The UI and export keep those limits visible.

Accomplishments

SimProof is a working teacher product rather than a verifier hidden behind a terminal. It has a library, generation lifecycle, repair evidence, accessible previews, version comparison, publication controls, export and deletion, backup and restore, and a reproducible Compose deployment.

The negative controls are permanent regression fixtures. The application rejects wrong formulas, unit mistakes, integration drift, stale evidence, hostile renderer content, runner escape attempts, and malformed process messages without weakening the policy to make a demo pass.

What I learned

Model output becomes more useful when its authority is narrow. GPT-5.6 is good at turning a teacher's intent into a structured request. Codex is good at producing and repairing a clean implementation from precise diagnostics. The trustworthy part comes from the boundary around them: independent policy, exact artifact identity, realistic negative controls, and failure states that stay distinct.

I also learned that accessibility belongs inside scientific correctness. A simulation is not useful to a teacher if its meaningful state exists only as an animation. The visible data representation is part of each supported domain, not an optional add-on.

What's next

Projectile motion and simple pendulum are the only supported generation domains. The next domain will be added only after its equations, bounds, invariants, tolerances, negative controls, renderer, and accessible data view pass the same review contract. The likely candidates are circuits and graphing, but they will not appear as supported until those packs exist.

I also want to make policy review easier for science educators by turning the current domain-pack evidence into a focused review interface without giving that interface a way to edit historical verification records.

Short testing note

The repository includes bundled projectile and pendulum examples, so judges can test the library, previews, data views, and reports without an OpenAI credential. Follow the README's supported setup. For a local walkthrough without an administrator password, use the committed compose.local-test.yaml override on loopback only. Live generation requires judge-supplied provider credentials; no credential or test account is included in the submission.

Built With

• codex