Verisyntax — User Manual (prototype 0.1)

Bayesian example without an LLM

p ~ beta(alpha = 2, beta = 2)
successes ~ binomial(trials = 20, probability = p)

observe successes = 14
ask p
  interval 0.89 hdi

The C++ runtime—not an LLM—calculates the posterior, HDI, effective sample size, split R-hat, acceptance rate, seed, and warnings.

Before warmup, unobserved normal parameters undergo a bounded deterministic density search from separate prior draws. During warmup, deterministic per-coordinate Robbins–Monro updates target 44% acceptance; proposal widths are frozen before retained sampling. This handles both remote posterior regions and posteriors much narrower than their priors. The JSON records initialization, warmupAdaptation, warmup and retained acceptance, and diagnosticsPassed. Retained posterior draws still come from the C++ Metropolis sampler. Regression tests cover both theta | measurement=1000 ~ normal(mean=500, variance=0.5) and two conflicting SD-0.1 sensors whose analytic posterior has mean 10 and variance 1/200.04; both must pass R-hat and ESS checks.

Logically impossible Boolean observations

If combined observations have probability zero under a Boolean model, a conditional posterior is mathematically undefined—not 0% or 100%. For example, observe disease = false and observe test_result = true are impossible together when the model declares P(test_result=true | disease=false)=0. The result dialog therefore shows Posterior is undefined / Logically impossible observations. Change or remove an observation, or use justified non-zero test error rates when the relationship is not truly perfect.

The result view uses adaptive precision near 0% and 100%. A small positive posterior such as 0.00000198 is therefore displayed as 0.00000198 (0.000198%) and must not look like the exact result 0. These small Boolean models use exact enumeration; MCMC, ESS, and R-hat are not involved.