From a request to a release

What must be provisioned

I’m building the system around an approved account of the machine and what it must do. Code, equipment versions, operating modes, signals, component documents and physical evidence give each check its meaning.

AI can expose ambiguities and explore failures. The responsible engineer approves the requirements. Changes to layout, equipment or operating limits need the accountable person’s approval; automatic software release requires an explicit customer policy.

For a fixture handshake, we need to know which request a confirmation belongs to, how long to wait and what happens after interruption. We must also examine unwanted behaviour that the rules permit. Contradictory assumptions, unreachable conditions and dropped requirements can make an empty result look successful.

What a proof can establish

A proof establishes that a precise claim follows from stated assumptions. To cover the program that will run, it needs a justified connection between implementation and model. Proving a rewritten controller alone proves something about the rewrite.

For each supported controller, we must account for its language, scan cycles, timers, arithmetic, scheduling and signal updates. Unsupported behaviour stays outside the claim or remains an open question. Digests identify exact source and executable bytes; the build and translation evidence explain how they relate.

Tests can support that connection. Cedar proves properties of Lean models and uses differential testing to connect them to production Rust. The evidence must preserve which part is proved and which is tested. FV03

Match each obligation to its method

The question chooses the tool. State-machine analysis suits handshakes; range analysis constrains possible values; logical solvers and proof assistants establish mathematical properties. Tests and measurements tell us about hardware.

A solver’s answer needs a checkable certificate or an explicit place in the trusted system. Functional correctness and termination are separate claims. Lean and Mathlib supply foundations; industrial meanings and interfaces still need engineering. Lean’s proof checking and executable compilation also carry distinct trust requirements. FV02

Protect the question and the gate

The required design separates authorship from approval. Customer agents propose software and deployment designs; Symbolia’s agents formalise requirements and prepare claims and evidence. Deterministic checkers use protected requirements, pinned tools and permitted assumptions. A submitted theorem cannot replace the one the customer approved.

Proof construction itself can execute code. Lean’s validation procedure therefore isolates construction and checks exported terms against a trusted statement. Multiple checkers can reduce implementation risk while still sharing a mistaken specification. FV01

Authenticated source authorship and independent approval must be enforced inside the core before the product can rely on that separation. The implementation record carries the current boundary.

Keep the core small and the knowledge reusable

One application will manage requirements, permissions, evidence and workflow. A separate process runs admitted checks. Every addition to the trusted core increases what we must maintain and qualify.

Customer models and numerical adapters can live outside it as versioned packages. Checkers cannot: each admitted method becomes part of the core and requires a new release that updates every customer partition’s binding. That is why I’ll qualify one robot method before funding another.

The first customer unit uses SQLite and immutable evidence files. We can change storage as workload demands without creating a second authority. Shared knowledge needs explicit ownership, permissions, versions and withdrawal rules at every scale.

Admit an execution, then inspect its result

An independent admission binds the exact inputs, checker, adapter and runtime. The operator runs that bounded package. The host checks the outputs against the admission before recording a conclusion.

Interrupted attempts remain visible. Retries preserve earlier evidence and prevent an old worker from completing a newer attempt. Local recovery and bounded-worker checks have been qualified; production isolation remains a separate requirement. SY01

Solvers can search for improvements within approved variables and objectives. Their answers still need checking. A sampled best point is the best among those samples; optimality requires a bound or certificate. Profit never gives a proposal authority to relax physical limits. The library’s own suggestion path remains to be implemented; the present path begins with a customer proposal.

Make composition explicit

A component’s guarantee depends on its surroundings. Two proved modules may still disagree about clocks, signal meanings or recovery. A claim about their combined behaviour must establish that they meet each other’s assumptions.

The graph records those relationships. A robot routine depends on a fixture contract; both depend on communication. A cycle of assumptions needs a joint argument. Recording the cycle does not supply one.

Physical motion also needs appropriate bounds, fault models and measured model error. Proof, numerical accuracy and physical applicability remain distinct parts of the argument.

Issue a package that survives a handover

The engineer needs six things: the exact system checked; the approved requirements; the supporting evidence; the assumptions and trusted tools; the conditions that keep the result applicable; and the recorded approval authority. The first engagement shows how these become a delivery.

People and customer agents receive the complete claim tree from one read of the same validated records. The human report preserves the conclusions without a model rewriting them. If the tree exceeds the reader’s limit, the reader refuses a partial display.

Each gap names the evidence or work needed to close it. The planned API lets the deployment submit that evidence for independent review, retaining its original kind. Its implementation depends on the author-approval boundary. A technical gap need not become a Director decision.

A CRITICAL finding identifies a supported obstacle to an approved requirement. A SUGGESTED improvement is optional. Missing evidence leaves a question open; it does not establish physical impossibility.

Keep evidence current as the machine changes

A replacement gripper can change response time. A new payload can invalidate a motion envelope while the software stays identical. I want the engineer to see which earlier conclusions need renewal.

The current implementation tracks affected artifacts. Connecting changes to individual obligations remains core work; until qualified, a patch re-checks everything in scope. The second deployment must measure the benefit of preserving unaffected evidence.

A changed model can also reveal dependencies the old graph missed. Keeping knowledge applicable is continuing engineering work.

At deployment, the customer’s gate checks the evidence against the intended machine configuration. Monitors can detect departures from observable assumptions. Essential protections and fallback remain local, with an installation-specific policy for lost connectivity and blocked unassured releases.

Give advanced controllers a bounded place to act

A capable controller can operate inside limits enforced by a simpler monitor and fallback. NASA’s runtime-assurance research examines intervention timing, recovery and the conditions that make recovery possible. Shared sensors, computing resources and hardware need analysis for failures that affect both controller and protection. FV14 FV15

This concentrates assurance around an inspectable boundary on what the controller can do.

Every guarantee needs a path back to the machine it describes. Every change needs a path forward to the evidence it must renew.