dawnr

dawnr combines local language models, program verification, and an assistant that works with code and documents. It generates candidate programs, tests their behavior and specifications, checks them with proof tools, and uses accepted results to build training data. The trained models can then propose new programs through the same checks.

The focus is better coding and reasoning through checked programs and better training data. Repository and document tools support that work. Controlling the whole computer is outside the project's scope.

The repository contains both the system and its working record: programs, contracts, deliberately broken variants, counterexamples, datasets, model-training code, evaluation scripts, and measured results. Its applications include checking selected PX4 flight-software routines against compiled C++ and recording proposed fixes alongside the inputs that expose the original failures.

Start in a terminal

git clone https://github.com/trestoncuzzort/dawnr
cd dawnr
./install.sh
export PATH="$HOME/.local/bin:$PATH"
dawnr doctor
dawnr do "Explain this project's structure and tests" --read-only

Run the last command inside the project you want help with. Models start automatically; the first installation downloads several gigabytes. Use dawnr for an interactive session, dawnr help ask for checked-code examples, or the user guide for setup and troubleshooting. You can read ./bin/dawnr --help before installing anything. Downloads come from the latest versioned release, now dawnr 6.0.1 (model card). Its model is the one first released on October 5, unchanged; the next model is in training as the 6.1.0 candidate and ships only if it beats this one (see the model status below). dawnr version prints the release a checkout is.

What is implemented

Part	What it does	Implementation
Program verification	Parses and checks t programs, translates them into proof-system inputs, and tests each verifier against a deliberately broken variant.	t/, t/run_par.py
Specification checks	Checks contracts against examples and reference behavior; mutates programs and outputs to find wrong results a contract still allows.	t/spec_gate.py, t/spec_check.py, t/audit.py
Executable comparisons	Compiles generated C or Dafny/Python and compares it with the interpreter. Separately checks C contracts and overflow obligations at machine width.	t/build.py, t/ship.py
PX4 checks	Models selected routines, records failing inputs and fixes, and compares them with compiled functions or extracted statements from checksum-verified source. Optional receipts identify each bounded run.	t/flight/
Native safety pilot	Uses CBMC to check the pinned original and fixed PX4 wrap_bin definitions under explicit 32-bit assumptions, with compiled counterexample replay and controls for vacuity and incomplete loop unwinding.	t/native_check.py, measured scope
Training and evaluation	Filters generated answers, assembles corpora, trains or fine-tunes models, and evaluates them with recorded splits, input hashes, and per-stage results.	t/student_rows.py, locallm/dawnr_pipeline.py, locallm/dawnr_report.py
Local assistant	Reads files, proposes edits, journals changes, runs sandboxed commands, and uses retrieval, memory, and external tools.	locallm/dawnr_cli.py, locallm/dawnr_agent/, locallm/dawnr_harness/
Documents and arithmetic	Answers with quotations from supplied files, extracts fields from source text, and compares a model's numerical answer with separately generated workings evaluated exactly.	locallm/cite_docs.py, locallm/extract_docs.py, locallm/calc.py

The dawnr command exposes the assistant and its checks in a terminal. A local browser interface, HTTP job API, and MCP server expose them to other clients. The command reference describes the individual entry points.

How code is checked

The verification language is t. A task states its inputs, preconditions (requires), postconditions (ensures), implementation, and any loop invariants. Its engine supports Dafny, Verus, SPARK, Frama-C, Lean 4, Rocq, and F*. Several front ends share underlying solvers; the reports identify the tools and versions that actually ran.

For a question with examples, dawnr ask runs this sequence:

1. Generate candidate t programs and reject ones that fail parsing, well-formedness checks, or the supplied tests.
2. Generate a separate Python solution and test it in a sandbox.
3. Check whether the candidate's specification agrees with that solution on sampled inputs and rejects mutated outputs.
4. Run available provers on the surviving program and a deliberately broken variant, with a concrete input that distinguishes the two. Report refutations, missing tools, unsupported constructs, and timeouts.
5. Translate an accepted program to Python and compare the translation with the t interpreter before returning it.

Other entry points reuse these components. dawnr prove starts from a supplied specification; dawnr verify uses an existing Python function as the behavioral reference. dawnr check replays a saved certificate's hashes, tests, prover checks, and executable comparisons without asking a model to regenerate the answer.

A proof establishes a property of the t program under its stated assumptions. The Python translation and PX4 correspondence are checked on bounded inputs. Specification checks can expose a mismatch with the intended behavior, but they cannot establish that the specification captures everything the user meant. These distinctions are part of the reported result.

The installed dawnr proof commands default to a minimum of one prover. An all-seven result must show seven successful program checks and seven refuted variants. The current engine pin is in t/ENGINE.md; engine development lives in t-proof-engine.

PX4 work in this repository

t/flight/ contains models of math helpers, filters, hysteresis, ring-buffer operations, collision-prevention indexing, and message-handler behavior. Findings include the failing contract and a concrete input; proposed fixes have separate tasks so the original and corrected behavior can be checked side by side.

Examples from the recorded, pinned PX4 revisions:

Case	Original behavior at the recorded input	Evidence
Obstacle-bin wrapping	Bin -73 with 72 bins returns -1, outside the valid index range.	Compiled-function comparison
SUMD channel decoding	A valid 32-channel frame reaches index 64 of a 64-byte buffer.	Finding and concrete input
Arming parameter conversion	Parameter 257 narrows to the arm action. The proposed fix rejects it.	Original and fixed statements
MAVLink serial control	A count of 71 exceeds the message's 70-byte data field. The proposed fix rejects that count.	Original and fixed statements

px4_diff.py compiles PX4's own routines and compares their outputs with the t models. px4_stmt.py compiles selected handler statements from original and proposed-fix revisions, with stand-ins for surrounding types and services. Each record names its revision, inputs, and comparison scope.

These checks cover the modeled routines and extracted statements. They do not establish correctness of the complete autopilot or behavior in flight. The numeric model also matters: many floating-point comparisons use binary64, while PX4 commonly uses binary32. The flight notes document those boundaries.

The data and model pipeline

Programs that pass checks feed corpus builders and training runs. Rejected programs, counterexamples, and verifier feedback are also used to construct and evaluate repair tasks. Held-out problems, contamination checks, and specification checks determine what a reported model result counts.

The resumable dawnr_pipeline.py driver covers tokenization, base training or an existing checkpoint, conversation construction, mid-training, optional supervised fine-tuning, evaluation, and reporting. Stage records contain input hashes and parameters; changed inputs invalidate downstream work. Its chat reinforcement-learning stage currently records a skip. Other experiments have their own drivers and records.

The installer supplies the dawnr 6.0.0 model, a fine-tuned Qwen3.5-4B, for program generation and a quantized base Qwen3.5-4B for the assistant and reference answers, served locally through llama.cpp. The repository also contains training code for models initialized from random weights. These are separate experimental paths; the installed model is described in the model card.

Results and corrections are kept in SCOREBOARD.md, docs/MEASURED.md, CORRECTIONS.md, and the linked experiment records. They describe particular runs and populations. Large weights and many generated run artifacts are downloaded or produced separately from a source checkout.

Model status, 2026-10-24

Releases are numbered dawnr MAJOR.MINOR.PATCH from 6.0.0. The released model is the October 5 model, carried unchanged in dawnr 6.0.0. A candidate is read against it alone: the count that matters is problems that pass their tests, the specification gates and all seven kernels from the frozen 17-call route ("clean"), on the 206 development problems no training row of the released model touches, two training seeds and three decodes each, paired per problem, never a verdict on a mean. The names v6 to v9 below are the names of measured experiments in their records.

model	training rows	clean / all-seven on the 95, one column per decode	record
dawnr 6.0.0, released (the October 5 model)	its own 5,095	6, 4, 6 / 3, 2, 3; 19.33 clean per decode on the 206	card
the "seed 2" model	the corrected 4,189, seed 2	4, 5, 4 / 2, 1, 1; 14.67 on the 206	seed variance
v6 corrective	the corrected 4,089	6 / 2	v6
v7	the corrected 4,089 plus decomposed rows	4 / 3	decomposed rows
v8	the corrected 4,089 plus 980 self-distilled specification rows	4, 4, 5 / 1, 2, 2	v8
v9	the corrected 4,189 plus self-distilled rows kept at a 90% strength floor	7 / 2, one decode	v9
6.1.0 candidate A	the October 5 model's own rows, audited, plus strictly checked specifications and repair examples	in training, seeds 1 and 2	registration

Corrected 2026-10-24: every candidate from v6 to v9, and the "seed 2" model, trained on a corrected set rather than the released model's own rows, and the 240-problem panel used to compare them held 34 problems the released model's rows had matched (CORRECTIONS.md). On the 206 unleaked problems the released model and the "seed 2" model read 19.33 and 14.67 clean per decode, permutation p 0.15, not separable. That is why 6.1.0 candidate A goes back to the released model's own rows. v8's rows did change one thing the count cannot see: the three-test gate's precision on the ceiling instrument fell from 0.785 to 0.515, so only self-distilled specifications that agree with the reference at 1,000 draws and reject 90% of both mutant families are kept (v9: 0.682). The next increment adds specifications written by Cohere's Command A models for the problems the model fails, kept only when the same checks pass, used with Cohere's written permission under a Cohere Labs Catalyst Grant. The plan is internal/RELEASE-6.0-PLAN.md.

Earlier: the October 11 GPU retrain trained on 405 rows from the recovered corpus, with 18 of 22 new verified answers represented (17 distinct additions). Four new answers overlap held-out specification functions and were excluded. The candidate proves 21/33 supplied specifications in all seven systems; the reference-program control passes all 33. On clean-182 programming problems, 4/182 pass the tests, specification gates and all seven kernels from one greedy answer; five reach at least six kernels. The VM and boot disk were deleted after the artifacts were saved. This smaller, single-answer experiment does not reproduce the October 5 model's training set or evaluation budget; that model remained the release.

Install and use

The application supports Linux, macOS, and Windows through WSL2, with Python 3.10 or newer. CPU inference is supported. The installer downloads the model server and models, checks their published checksums, installs Dafny where supported, and adds dawnr to ~/.local/bin. Other proof backends have separate setup instructions in t/README.md.

git clone https://github.com/trestoncuzzort/dawnr
cd dawnr
./install.sh
dawnr doctor

On a fresh Ubuntu installation, the installer may require libgomp1, unzip, and bubblewrap. Commands that execute generated Python require a working sandbox. See the installation guide for setup, model storage, and platform-specific requirements.

# Generate a checked function and save its replayable record.
dawnr ask "Write a function that returns the larger of two integers." \
  --test "assert larger(3, 5) == 5" --test "assert larger(9, 2) == 9" \
  --save-python larger.py --certificate larger.cert.json
dawnr check larger.cert.json

# Work with a folder or ask a question about a document.
dawnr do "Describe the modules in this repository." --read-only
dawnr cite "What does a comparison receipt not capture?" t/flight/README.md
dawnr calc "A logger records 12 samples per second for 15 seconds. How many samples is that?"

The repository assistant defaults to local models and offline operation. Its file tools support reviewed edit plans and a change journal; /undo restores recorded changes. Built-in desktop and host-service control is retired. Read-only build-environment diagnostics remain available; repository commands require a working sandbox. --online enables the assistant's network tools, and DAWNR_WRITER_URL can select an external model for program generation. Those options change what stays local. See PRIVACY.md and DAWNR-AGENT.md.

Run existing verification tasks without a model

The parser, interpreter, and mutation audit can run directly from the source checkout. Formal checks need the selected prover installed and on PATH; compiled comparisons also need the relevant compiler.

python3 t/cli.py check t/flight/fixes/px4_wrap_bin_fixed_72.t
python3 t/cli.py audit t/flight/fixes/px4_wrap_bin_fixed_72.t --json

# A proof and its deliberately broken variant, using Dafny.
T_MIN_KERNELS=1 python3 t/cli.py verify \
  t/flight/fixes/px4_wrap_bin_fixed_72.t --kernels dafny --json

# Refute the original contract at a recorded failing input.
python3 t/refute_at.py t/flight/findings/px4_wrap_bin_any.t \
  --at '{"bin": -73, "bin_count": 72}' --kernels dafny --json

# Compile and compare checksum-verified PX4 sources; fetches source when absent.
python3 t/flight/px4_diff.py --table /tmp/dawnr-px4-diff.md \
  --receipt /tmp/dawnr-px4-diff.json

# Experimental native safety check; requires CBMC 6.11.0 and a C preprocessor.
python3 t/native_check.py --case fixed --out /tmp/dawnr-native-fixed

The engine CLI also exposes lowering, contract repair, compiled-output comparisons, and machine-width checks: python3 t/cli.py --help. Reports and certificates retain the scope of the checks that ran; an unavailable or unfinished check does not count as a pass. The native pilot is separate from the seven proof backends: its complete verdict covers the listed safety properties for all modeled 32-bit bin inputs with a bin count of 72. It does not establish the full modulo specification or whole-module correctness.

Repository map

Path	Contents
bin/dawnr, install.sh	Application launcher, local model serving, and installation.
t/	Pinned proof engine plus dawnr's generation, data-filtering, and evaluation scripts.
t/flight/	PX4 models, findings, proposed fixes, and source-comparison harnesses.
locallm/	Model and training code, the assistant, document tools, retrieval, memory, and evaluations.
nl/	Programming-problem datasets and their preparation records.
release/	Model cards and release documentation.
docs/	Command reference, user guide, and measurements.
internal/	Research notes, design records, and historical handoffs.

For development, see CONTRIBUTING.md. For recorded limitations and reporting defects, see LIMITS.md, DISCLAIMERS.md, and SECURITY.md.

License

Research and education use only; see LICENSE and DISCLAIMERS.md.

Copyright (c) 2026 Treston Malachi Cuzzort.