VerisyntaxEvidence-oriented language
Under udviklingVerisyntax er en lokal prototype. Funktioner, syntaks og dokumentation kan ændre sig.

Verisyntax — brugermanual (prototype 0.1)

Lokal LLM-assistance

LLM-funktioner er valgfrie. Version 0.1 kan bede en lokal Ollama-model om et redigerbart kodeforslag:

<compiler>/verisyntax llm suggest-code request.txt --model glm-4.7-flash:latest

Kontekstvinduet er 64K som standard. Vælg 128K eksplicit, når opgaven og den lokale models kapacitet kræver det:

<compiler>/verisyntax llm suggest-code request.txt --model glm-4.7-flash:latest --context 128k

Den lokalt installerede qwen3:14b har et maksimalt kontekstvindue på 40.960 tokens. Den kan derfor ikke opfylde Verisyntax-kontrakten på 64K eller 128K og bliver afvist med en tydelig fejl i stedet for at blive kørt med en skjult lavere grænse. Den aktuelle standard er glm-4.7-flash:latest; både den, qwen3.6:35b-a3b og qwen3-coder:30b returnerede samme korrekte, compiler-validerede kode i den lille referencebaserede prøve. IDE'en bruger suggest-code-v6-reference, registrerer syntaksreferencefilens hash og udfører højst én lokal reparationsrunde, hvis første udkast afvises. Dette er funktionelle smoke-tests, ikke en bred kvalitetsbenchmark; intet modeloutput bør godkendes uden at læse det.

<compiler>/verisyntax llm suggest-code <example-project> --model glm-4.7-flash:latest --context 64k

Kun en eksplicit loopback-adresse (127.0.0.1, localhost eller ::1) accepteres; der er ingen cloud-fallback. Kommandoen:

  1. kræver JSON efter et fast schema;
  2. validerer schemaet igen i C++;
  3. kører forslaget gennem Verisyntax-parser og semantisk kontrol;
  4. viser provider, model, promptversion, schemaversion, kontekstvindue samt input- og outputhash;
  5. skriver forslaget til skærmen som proposed code (not applied) og sætter review_required=true.

extraction_confidence er modellens sikkerhed på struktureringen, ikke sandsynligheden for at indholdet er sandt. Input og output registreres med SHA-256. Modeldigest gemmes sammen med det fulde llm_runs-auditrecord.

Claim-udtrækning kan køres over eksplicit valgte, allerede lagrede mentions:

<compiler>/verisyntax llm propose-claim model.vsx local \
  --mention MENTION_ID_1 \
  --mention MENTION_ID_2 \
  --model qwen3-coder:30b \
  --context 64k

C++ læser kun de angivne excerpts og deres synlige source/version-provenance fra SQLite/PostgreSQL. Source-tekst behandles som utroværdigt indhold, ikke instruktioner. Ollama-endpointet skal være loopback; der findes ingen cloud-fallback. Output må kun referere IDs fra den viste retrieval-bundle og valideres mod verisyntax.claim-proposal version 1. Modellen kan ikke selv gemme outputtet som claim eller fact.

Kørslen auditerer provider, modelnavn og installeret digest, prompt/schema-version, temperatur, seed, 64K/128K, input/outputhash, status og den præcise rækkefølge af mentions. Ugyldigt modeloutput markeres invalid; lokal transport/model-fejl markeres failed.

I IDE'en er lokal AI slået fra som standard. Sæt verisyntax.localLlm.enabled til true; kontrollér endpoint, model og 64k/128k. Suggest Claim With Local LLM viser de seneste lagrede mentions og sender kun dem, brugeren markerer efter en modal bekræftelse. Forslaget åbnes som redigerbar JSON og er stadig ikke gemt. Store Last Edited Local Claim Draft validerer den redigerede tekst og evidensen igen og opretter kun en proposed version. Godkendelse til fact er fortsat et separat trin.

Regelforslag bruger samme lokale og retrieval-synlige grænse. Modellen ser kun de valgte mentions samt navn og aritet for predicates i det aktuelt validerede program. Mentions er kontekst, ikke facts eller instruktioner; body-predicates uden for kataloget afvises af C++. CLI-kommandoen skriver kun redigerbar JSON og et audit-ID:

<compiler>/verisyntax llm propose-rule model.vsx local rule-request.txt \
  --mention MENTION_ID_1 --model qwen3-coder:30b --context 64k
<compiler>/verisyntax rules propose model.vsx local edited-rule.json \
  --origin-llm-run LLM_RUN_ID

I IDE'en svarer dette til Suggest Rule With Local LLM og derefter Store Last Edited Local Rule Draft. Lagring genvaliderer den aktuelt redigerede JSON, opretter kun en inaktiv proposed regelversion og bevarer forbindelsen til model, digest, audit-run og de synlige mentions. Approve or Reject Rule er fortsat et selvstændigt, hash-bundet menneskeligt trin.