The problems of provable (formally-verifiable) program safety and determinism became crucial in the age of modern LLMs. I am developing #AluVM and @CationLang as a constructionist and ultrafinitist tool: in each type is a finite set of constructable objects; so there is type N8 made of all natural numbers (0 is not natural!) in range 1-256 included, N16, N32 and N64. There are integers of the same sort (0 included), I8, I16, I32 etc. There are no floating-point numbers, only rationals (in the Norman Wildberger @n_wildberger style), no sine/cosine - only rational trigonometry. Integers are pairs of numbers, not just “unsigned with a sign bit”, rationals are pairs of integers (i.e. quadriples of numbers). It uses dependent types (calculus of constructs), but restricts to finite types only. All functions are total, the termination analysis proves that. There is no recursion which can’t be reduced to a provable-terminating computation at compile-time. This gives a language and computational system which is formally analyzable at compile-time, by its structure.additionally to that, a binary compiled code is also formally analyzable and has a verifiable properties.