Parsing, formatting, and diagnostics for Mission-time Linear Temporal Logic.
The v0.1 boundary uses the independently authored, versioned ASCII dialect in
docs/DIALECT-001-clean-room-mltl-v1.md.
It maps source directly into the exact pinned tl-syntax graph model and does
not own a second AST or temporal semantics.
The crate compiles against tl-syntax at
26b801d4a68ebfe720062cfdb3c66b070ab60e92, an exact commit reachable from the
reviewed main history when admitted, not a moving branch head. That revision
carries the contextual and semantic contracts. The dialect was authored from
the earlier revision 740182f1, which is
a separate and historical fact; docs/ATTRIBUTION.md records both, and
Cargo.lock is what enforces the compiled one. The dependency still resolves by
exact git revision because
tl-syntax has no registry release, and source release remains blocked while
that is true.
make cimake ci is the complete local iteration gate. Hosted GitHub Actions is
manual-only (workflow_dispatch) and is deliberately run only for a finalized
PR revision.
The thin CLI accepts a file or stdin:
cargo run --bin tl-parse -- validate --profile closed formula.mltl
printf 'p0 U[1,2] true' | cargo run --bin tl-parse -- format --profile online -The checksum-protected hostile-input corpus is in corpus/v1; fuzz seeds and
the cargo-fuzz target are under fuzz/.
Verification results are produced by this repository's own tools, transcribed
and retained by Quoin, and described by
static facts exported from Quire.
Neither tool executes a producer. make assurance classifies the toolchain
through the packaged Engineering Assurance compatibility matrix and drives the
seal/intake/receipt chain.
This repository retains no evidence of its own. Verification evidence is what the chain produces at the reviewed revision; Git history and pull-request review are the integrity boundary for the source.
Its public API is not stable yet, and registry publication is disabled until the v0.1 assurance review is complete.
Agent-assisted contributions are reviewed under the same requirements, testing, provenance, and human release gates as every other contribution.
Licensed under either of Apache License, Version 2.0 or MIT license at your option.