Inspiration
Security assurance is usually expressed in prose, spreadsheets, or generic configuration. Those formats make it easy to treat the existence of evidence as proof of compliance, ignore who is responsible for a control, or hide uncertainty behind a pass/fail result.
VerityScript explores a different approach: make evidence provenance, authority, assumptions, defeaters, and unresolved conclusions first-class language concepts.
What it does
VerityScript lets users express security obligations and the evidence needed to support them. A compiler validates the program before generating structured assurance JSON and a human-readable evidence plan.
Its central rule is simple: unsupported assurance conclusions should be difficult to express. Technical evidence must identify who controls it, and a strong conclusion requires evidence controlled by the responsible actor or shared responsibility. Provider evidence, for example, cannot silently prove that a customer or supplier operated its own control.
Ontologies describe assurance concepts, graphs connect them, vector stores retrieve relevant material, and agent memory retains context. VerityScript provides the executable authoring layer that checks whether a proposed assurance conclusion is structurally consistent with the declared evidence, responsible actor, evidence controller, and unresolved uncertainty.
These technologies can complement the compiler as inputs or future output targets. The .verity source remains the reviewable and reproducible statement of intent; the compiler validates the assurance model but does not independently collect evidence or prove that an external observation is true.
How we built it
VerityScript is implemented from scratch in TypeScript with no runtime package dependencies. Source passes through a handwritten lexer and recursive-descent parser into a typed abstract syntax tree. A separate semantic checker applies assurance-domain rules before either compiler backend can run.
Diagnostics carry stable error codes and source spans. The CLI exposes check, compile, format, and explain, with deterministic assurance JSON and Markdown targets. Strict TypeScript checking and Node's built-in test runner cover tokenisation, parsing, unsafe assurance states, ownership compatibility, compiler determinism, diagnostics, formatting, Markdown safety, and CLI exit behaviour. The complete clean-install verification also runs in GitHub Actions.
Challenges we ran into
The hardest design problem was deciding what the compiler is allowed to infer. Evidence that another party has a capability does not prove that the actor responsible for an obligation configured or operated it. Likewise, technical evidence may support a security conclusion without authorising a legal or compliance conclusion.
We encoded those boundaries as semantic rules for supplier, customer, provider, regulator, and organisation actors. Every technical evidence block identifies a recognised controller; shared evidence can support any actor, while external remains valid provenance without automatically establishing an actor-owned control. Adapter-specific evidence fields remain extensible and uninterpreted by the current checker.
The MVP is scoped to operational security-control conclusions. Documentary, provider, and human evidence can supplement a compatible technical basis but cannot independently support documentary-only obligations yet. Explicit requirement kinds are the planned extension point for technical controls, documentary obligations, and compliance claims.
Ontology and graph-validation systems can express sophisticated constraints. Our claim is narrower: they are less suitable as the primary practitioner-facing authoring and compiler experience for this domain, where concise source, line-and-column diagnostics, deterministic output, and version-control review matter.
Accomplishments that we're proud of
- A complete handwritten lexer and parser with line/column diagnostics.
- A conclusion lattice that rejects satisfied security without supported evidence and verified compliance without satisfied security.
- Actor-general responsibility checks: strong conclusions require technical evidence controlled by the responsible actor or shared responsibility.
- Required, validated technical-evidence controllers covering supplier, customer, provider, regulator, organisation, shared, and external provenance.
- A closed actor domain that prevents responsibility checks being bypassed with arbitrary aliases.
- Meaningful human compliance assertions with reviewer, assertion, review date, scope, and accepted authority.
- Deterministic assurance JSON and Markdown, plus canonical VerityScript formatting and safe Markdown escaping.
- Three realistic example programs, an intentional failure demonstration, and 38 automated tests.
- A runtime-dependency-free Node.js 24 CLI with strict type-checking and a green hosted CI workflow.
- An MIT-licensed implementation created for Syntax Summit.
What we learned
A small DSL becomes useful when its invalid states reflect real domain mistakes, not just syntax mistakes. Separating parsing from semantic checking made the implementation easier to explain and allowed diagnostics to teach the assurance model. Explicit undetermined results are also more informative than forcing every obligation into pass or fail.
What's next
Potential extensions include reusable evidence templates, richer authority types, explicit requirement kinds for documentary obligations and compliance claims, OSCAL or SARIF output, Veritylane-compatible JSON, editor support, knowledge-graph output, and evidence-collector integrations.
Log in or sign up for Devpost to join the conversation.