InferenceLang

@InferenceLang: A programming language, compiler, and SI-powered proof discovery system. We started R&D for this project before formal verification became popular among SI companies on X. Our compiler can do auto-formalization at compile time, which means the only job for SI is to discover proofs. This is much faster and token-efficient than just asking a model to formalize something and then prove it. Incomparably more efficient.

A program can compile and pass its tests, yet still make a dangerous decision. For software controlling a satellite or moving money, that gap matters. We're building @InferenceLang, a programming language and verification system that helps engineers prove their critical software rules hold. Imagine a satellite payload that may switch on only when its battery, temperature, and operating mode are safe. Inference lets the engineer write that requirement as a precise specification alongside the code. The compiler produces executable WebAssembly and formal proof obligations: mathematical statements that must be proved. Our AI prover attempts those proofs, and an independent verifier checks the results using Rocq, a mathematical proof checker. The AI proposes the proof; it does not decide whether the proof is valid. That combination is our approach: a language designed for verification, a compiler that generates the mathematical statements to prove, and AI assistance for the difficult proof work. Our goal is to make rigorous verification practical for engineers who are not theorem-prover specialists. We focus on critical decision logic, such as command authorization, safety interlocks and state transitions. We're not claiming to prove an entire spacecraft or an AI model safe. A successful proof establishes a specific property under explicit assumptions. For teams using AI to write code, this offers a way to demand evidence that the result meets a specification, rather than relying on a convincing explanation. It complements testing with a different kind of assurance.

Opus 5.5. is also good in using @InferenceLang

My team has been working on @InferenceLang for several years already. With Inference language, it is possible to compile code to WebAssembly and automatically generate formalization for a theorem prover. The halting problem is solved classically by giving an execution fuel it consumes until ran out of it, then — unreachable ∎

inference-lang.org is designed specifically to put formal methods in the hands of all developers who can read and write C-style languages. @InferenceLang is open source. Contributions are welcome. github.com/Inferara/inferenc…

Read it if you are interested in compilers and formal verification

First ever comp time operational semantics auto formalization and lowering.

Leave No Room for Errors: How @InferenceLang is Bringing Accessible Theorem Proving to @StellarOrg medium.com/@inferara/leave-n…

Enums support is added to @InferenceLang github.com/Inferara/inferenc…, but enums in Inference are mostly close to the Clang enum (which actually does not have enums and named literals are just macros). So enums are more for type-checking and better code organization, low level enums are i32.

Nested compound types (structs) and multidimensional arrays support have been added to @InferenceLang github.com/Inferara/inferenc…

Added struct methods call lowering for @InferenceLang, helping to aggregate data in logical structures and combine operations on them: github.com/Inferara/inferenc… However, Inference follows NASA grade code quality rules so that: 1. Method call chunks are not supported (a.b().c()); this is because such things make code less readable, and a potential error can occur;, 2. Methods returning structs or arrays cannot be called directly in the function call foo(bar()); the reason is that bar returns an entity that requires memory layout preparation. It can be done during codegen, but it actually hides memory operations from the user. This is a bad practice, so the right pattern is let my_struct = bar(); foo(mu_struct); The next PR will add more validation rules to make Inference safe to use. Stay tuned.

Another big milestone of @InferenceLang was successfully achieved and with the last ingredient in the dish (linear memory arrays) the practical Turing completeness was achieved. This is huge imo. What does it mean in practice? Well, a Turing machine is a machine with an infinite tape, memory, and commands sequence which switch from the current to the next state (memory, basically). Ok, now in practice. It means that now in Inference can be written any algorithm (program) from calculator to operating system. For Inference, we want to write formal specifications and lower them in compile time to ATP (automated theorem prover) code. This is our next big milestone. But at the same time. We can @BuildOnStellar critical software like @StellarOrg smart contracts in Inference and the binary will be smaller/more optimized than rust one. Why is it? Because llvm lowering is a general purpose thing. Inference custom lowering controls every detail. For example, memory allocation. If we statically know we do not need more than 1 page, we will not allocate more, and if we do not need _memory, we can skip its allocation at all. Imagine only stack based calculations in libraries. More details I am adding into the compiler book github.com/Inferara/inferenc…

@InferenceLang is designed to auto formalization so that theorem definitions, and the whole theory can be expressed in imperative manner and lowering to ATP is done in comp time

@InferenceLang has compile time autoformalization