Research StarLang verification experiment program #117

Merged

lost-rob0t merged 9 commits from agent/star-lang-verification-experiment-research into main

2026-08-15 15:48:39 +00:00

lost-rob0t commented

2026-08-15 15:27:52 +00:00

(Migrated from github.com)

What changed

Adds STAR-LANG-RESEARCH-025 Verification Experiment Program for Actor Ingest as the direct experimental follow-up to STAR-LANG-RESEARCH-024.
Grounds all ten required experiments in the current star-lang runtime/protocol/transport source instead of a hypothetical API.
Adds durable formal research fixtures under experiments/star-lang/verification/:
- StarActorIngest.tla
- StarActorIngest.cfg
- person-minor-unsat.smt2
Updates the canonical StarLang research index with RESEARCH-024 and RESEARCH-025.
Leaves research conclusions PENDING; this PR does not approve implementation architecture merely because the experiments ran.

Runtime finding

Current starlang-runtime:ask is mailbox-backed but still synchronous while called from inside an actor handler. In an A→B→A cycle, A remains busy, B's nested request cannot re-enter A because of the existing processing-p guard, and the nested ask eventually fails by deterministic timeout. That is bounded failure, not the split-phase mailbox-progress guarantee required by STAR-SERVER-033.

Executed TLA+/TLC evidence

Formal research run: 31893307344.

The first TLC attempt exposed a model defect: terminal quarantined quiescence had not been represented explicitly and was reported as deadlock. The model was repaired by making terminal quiescence explicit.

The successful run used TLC2 2.19 from the pinned TLA+ v1.7.4 tla2tools.jar and checked the complete bounded research state space:

83 states generated
40 distinct states
depth 13
0 states left on queue
safety invariants passed
temporal property passed
Model checking completed. No error has been found.

Fixture hashes:

StarActorIngest.tla: 2329f5c90c1086d946dad1d740f326181cdb52dd5c3e575f35353e19e909eea6
StarActorIngest.cfg: 452e1eccbc0234c17b056b37ffc799679e3e00c3fb33a7901db2a098888a2883
tla2tools.jar SHA1: bee4a54f3ee3d4afc347c3240ec2d9e93b075104

This is bounded model-checked research evidence for the fixture, not an unrestricted theorem and not yet a production deployment certificate.

Executed SMT/Alethe evidence

The Person age/minor QF_LIA fixture was executed with cvc5 1.3.4:

cvc5 result: unsat
SMT input SHA256: 9d3ec57479f75a503f69d2f5bcbad0fd078b73bee2a90157779712c54d68fc81
Alethe proof SHA256: 3a6bf20e254fe9dd51527b85b19700ef835b7988ecdef792ee73fc35e2791aa3
pinned Carcara: 1.1.0 at commit 6624ea80cf1985ada473c0705869c78353e4282d
independent Carcara check exit code: 0

The formal evidence upload is Actions artifact 9249135467; its uploaded ZIP SHA256 is ac263f16435979a36ced7ec5f7f9be6c4d141cfed2ac5d46dfa2fed3acb7987e.

Trust boundary

The formal results establish feasibility and evidence shape. They do not prove arbitrary Common Lisp code deadlock-free, do not prove arbitrary StarIntel plans, and do not make schema validity equivalent to factual truth. Production P3 evidence still requires deterministic generation from the actual immutable execution plan, exact bounds/assumptions, and retained checker/model hashes.

The temporary branch-only formal execution workflow used to obtain the evidence was removed before merge; no parallel permanent CI framework is introduced.

## What changed - Adds `STAR-LANG-RESEARCH-025 Verification Experiment Program for Actor Ingest` as the direct experimental follow-up to STAR-LANG-RESEARCH-024. - Grounds all ten required experiments in the current `star-lang` runtime/protocol/transport source instead of a hypothetical API. - Adds durable formal research fixtures under `experiments/star-lang/verification/`: - `StarActorIngest.tla` - `StarActorIngest.cfg` - `person-minor-unsat.smt2` - Updates the canonical StarLang research index with RESEARCH-024 and RESEARCH-025. - Leaves research conclusions `PENDING`; this PR does not approve implementation architecture merely because the experiments ran. ## Runtime finding Current `starlang-runtime:ask` is mailbox-backed but still synchronous while called from inside an actor handler. In an A→B→A cycle, A remains busy, B's nested request cannot re-enter A because of the existing `processing-p` guard, and the nested ask eventually fails by deterministic timeout. That is bounded failure, not the split-phase mailbox-progress guarantee required by STAR-SERVER-033. ## Executed TLA+/TLC evidence Formal research run: `31893307344`. The first TLC attempt exposed a model defect: terminal `quarantined` quiescence had not been represented explicitly and was reported as deadlock. The model was repaired by making terminal quiescence explicit. The successful run used TLC2 2.19 from the pinned TLA+ v1.7.4 `tla2tools.jar` and checked the complete bounded research state space: - 83 states generated - 40 distinct states - depth 13 - 0 states left on queue - safety invariants passed - temporal property passed - `Model checking completed. No error has been found.` Fixture hashes: - `StarActorIngest.tla`: `2329f5c90c1086d946dad1d740f326181cdb52dd5c3e575f35353e19e909eea6` - `StarActorIngest.cfg`: `452e1eccbc0234c17b056b37ffc799679e3e00c3fb33a7901db2a098888a2883` - `tla2tools.jar` SHA1: `bee4a54f3ee3d4afc347c3240ec2d9e93b075104` This is bounded `model-checked` research evidence for the fixture, not an unrestricted theorem and not yet a production deployment certificate. ## Executed SMT/Alethe evidence The Person age/minor QF_LIA fixture was executed with cvc5 1.3.4: - cvc5 result: `unsat` - SMT input SHA256: `9d3ec57479f75a503f69d2f5bcbad0fd078b73bee2a90157779712c54d68fc81` - Alethe proof SHA256: `3a6bf20e254fe9dd51527b85b19700ef835b7988ecdef792ee73fc35e2791aa3` - pinned Carcara: 1.1.0 at commit `6624ea80cf1985ada473c0705869c78353e4282d` - independent Carcara check exit code: `0` The formal evidence upload is Actions artifact `9249135467`; its uploaded ZIP SHA256 is `ac263f16435979a36ced7ec5f7f9be6c4d141cfed2ac5d46dfa2fed3acb7987e`. ## Trust boundary The formal results establish feasibility and evidence shape. They do **not** prove arbitrary Common Lisp code deadlock-free, do not prove arbitrary StarIntel plans, and do not make schema validity equivalent to factual truth. Production P3 evidence still requires deterministic generation from the actual immutable execution plan, exact bounds/assumptions, and retained checker/model hashes. The temporary branch-only formal execution workflow used to obtain the evidence was removed before merge; no parallel permanent CI framework is introduced.