Get started
Welcome to Refinery
Refinery is independent verification infrastructure for consequential software. It determines whether a proposed change preserves behaviour, maps what the change can affect, and produces evidence a risk owner can approve.
Run an audit →
Compare original and modified COBOL through one repeatable workflow.
Understand the decision →
See exactly what turns a verification result into PASS or FLAGGED.
Inspect the evidence →
Learn what is signed, fingerprinted and retained for review.
Choose an interface →
Use the CLI, API or governance portal around the same engine.
Quickstart
Run your first comparison
Clone the repository, install the Python environment with uv, then submit the original and modified programs to the audit engine.
uv sync --dev
uv run python -m audit original.cob modified.cob --output report.pdfThe command returns a machine-readable verdict and writes the signed PDF Change Contract to the requested path.
Workflow
From code change to governed decision
Submit both versions
Provide the original program and the proposed change. Refinery fingerprints both inputs before analysis begins.
Run independent verification
Deterministic checks, compiler-grade semantic analysis, estate mapping and formal proof run outside the tool that wrote the change.
Make the release decision
A PASS can proceed. Material findings close the release gate and route the evidence to a named approver.
Retain the evidence
The signed Change Contract and evidence pack preserve what ran, what was found and who approved the decision.
Verdicts and gates
A decision, not another dashboard
A clean run returns PASS. Any high- or medium-severity behavioural finding returns FLAGGED and closes the promotion gate. Unsupported proof scopes are reported as out of scope—never presented as proof.
PASS
All active checks completed without a material finding. Evidence is issued with the result.
FLAGGED
A material change requires remediation, documented acceptance, or a named human sign-off.
Evidence and signing
Every decision leaves a verifiable record
The Change Contract records input fingerprints, active checks, findings, proof status, estate impact, provenance and approval. Its SHA-256 fingerprint makes later tampering detectable, while the evidence pack preserves the supporting machine-readable artefacts.
CLI and API
One engine, multiple interfaces
Use the command line in CI, the API for system integration, or the governance portal for human review. Each surface calls the same audit engine.
# Public API wrapper
uv run uvicorn api.main:app --reload --port 8000
# Governance portal
uv run uvicorn portal.main:app --reload --port 8080Governance workflow
Human authority stays explicit
Refinery can recommend and explain, but AI-generated narrative is excluded from the signed attestation. Material risk acceptance ends with a named human decision, recorded with the audit evidence.
Deployment model
Designed for controlled environments
The deterministic audit and proof layers run offline. Enterprise deployments can keep source, audit records and local AI inference inside the customer environment, including air-gapped operation.
Verification layers
Defence in depth
Deterministic checks
Eleven named checks cover arithmetic drift, data declarations, control flow, exception paths, I/O order, dataflow and formal equivalence.
Semantic engine
A compiler-style pipeline resolves symbols, expands copybooks and analyses whole-program control and data flow.
Formal verification
Z3 proves supported arithmetic and conditional transformations equivalent, or returns a concrete counterexample.
Estate impact
Callers, JCL, copybooks and VSAM relationships define the systems requiring review.
Proof scope
Honest results when proof is not possible
A proof result applies only to the statements and semantics the solver model supports. Unsupported constructs, timeouts and unavailable dependencies produce explicit OUT_OF_SCOPE or UNAVAILABLE results rather than a false PASS.