Neutron Lean
Prove the rules your application depends on. The verification framework for Neutron’s multi-language ecosystem — bringing Lean models, reusable proofs, and application contracts into one development workflow.
One ecosystem. A language for correctness.
Neutron gives each language a role: TypeScript for interfaces, Go and Rust for services, Python for AI applications, and specialist libraries for scientific computing and ML. The application frameworks share a behavioral contract and connect to Nucleus through its PostgreSQL wire protocol.
Lean adds a place to express the rules those applications depend on: valid state transitions, authorization decisions, resource limits, and the properties of core algorithms. The planned framework brings that work into Neutron projects as a reusable component alongside the languages that run the application.
Coming soon: application-facing proof libraries, connections to the language SDKs, and integrated build tooling are planned. The Nucleus algorithm-model proof suite is available today.
Define. Prove. Connect.
The intended workflow starts with a small, explicit model of an important rule. Prove the properties that rule must preserve, then connect the model to the application through implementation checks. Keep the model, assumptions, and implementation checks together as the application changes.
From a business rule to a checked model.
Consider an inventory service written in Go with a TypeScript storefront. The intended Lean workflow would model reservations and cancellations, then prove that accepted operations preserve the model’s stock limits. Integration checks would exercise the Go service against that model.
The proof establishes a property of the Lean model under its assumptions. Tests, implementation review, and any future verified translation establish how the running service relates to that model. Sharing Nucleus or an API contract alone does not transfer a proof to another language.
A foundation you can inspect today.
The repository already contains hand-written Lean models and proofs for Nucleus algorithms, including MVCC visibility, B-tree structure, write-ahead logging, caching, and cryptographic constructions. The suite uses Lean’s kernel to check proofs and an axiom audit to track their assumptions.
These are proofs about algorithm models. They do not certify the shipping Nucleus binary or application code. The broader Neutron Lean framework will build on this foundation; its application integrations are still to be built.
Read the current suite documentation or inspect the models and proofs.
Verification that fits the whole system.
Explore the proposed architecture for proof libraries, language adapters, and reproducible evidence across Neutron.
Lean’s proposed role is reusable models and deductive proofs. Quint models stateful protocols, while Verus supports verification of annotated Rust. Neutron Lean is intended to connect proof work to the wider development experience, with each tool’s scope and assumptions kept explicit.
The planned release includes project setup, reusable application models, language integration examples, and build checks. APIs and language coverage will be documented as those integrations are implemented.