Loading...
Supporting developers, startups, and full-fledged companies building on Stellar and Soroban
© 2025 Stellar Development Foundation
Subscribe to the Newsletter
By Inference
Theorem provers are the most powerful tools for finding errors in code. But without specific expertise it is extremely difficult to effectively use it. We make theorem provers power accessible to all Stellar developers.
To view this entire application easily with additional reference images please view it directly here via google docs.
As new milestones are being reached for Stellar such as the $30m in TVL of Aquarius, and $150m TVL total on-chain, there should be additional preparations to ensure the continuous security of user assets.
There are several companies that analyze code for protocols using Soroban and other blockchains. Inferara provides an innovative solution that is designed specifically to be used by developers to further increase the security of user assets.
The standard methods for finding bugs and overall correctness of code is often achieved through unit tests, fuzz and invariant tests as well as integration tests. These are useful and are effective at proving the presence of bugs, but it can not prove their absence!
We propose a different method of formal verification that is not bound to these traditional methodologies. This is done via Inference.
Inference is designed as a domain‑specific formal specification language for Web3 native applications. Its syntax is concise and Rust‑like, and it aims to let developers write formal specifications, align them against assumptions of the Soroban framework and automatically generate Rocq (formerly named Coq) theorems. Inference seeks to bridge the gap between theorem proving and practical application development in blockchains. Inference provides a proof-ready notation for developers to define contract invariants and properties. Instead of writing an ambiguous sentence like "the total supply should not change," a developer writes a precise, mechanizable specification in Inference. This approach provides a way to integrate formal verification into the development process of Stellar projects.
The key difference between unit tests and properties defined by Inference is that unit tests check correctness at certain points (a set of particular inputs), while the properties defined by Inference can check correctness for all possible inputs.
For example, consider specifying that an is_prime function correctly checks the primacy of all possible numbers. In unit tests, you might write tests for specific inputs like this:
fn test_primes() {
assert_eq!(is_prime(13), true);
assert_eq!(is_prime(21), false);
}
In Inference, you can write a specification that asserts the correctness of is_prime for all inputs:\
external fn is_prime(n: u64) -> bool;
fn prime_spec() forall {
let n: u64 = @;
assume { assert!(n > 1); }
if is_prime(n) {
let m: u64 = @;
assume { assert!(m > 1 && m < n); }
assert!(n % m > 0);
} else exists {
let m: u64 = @;
assert!(m > 1 && m < n);
assert_eq!(n % m, 0);
}
}
fn proof() {
prime_spec();
}
In this example, prime_spec is a forall-marked function that, using the @ (uzumaki 渦巻) keyword, says that with every n (unsigned 64-bit integer) succeeding assertion of n > 1, call to is_prime(n) is indeed returning its primacy. For prime n, dividing it by every m that is m > 1 && m < n must result in a non-zero remainder. For composite n, there must exist such m (again, m > 1 && m < n), that is a divisor of n.
Keep in mind this is a brief example to convey the power of inference. If you are interested in a deep dive, we highly recommend reading the inference language spec on our github.
Inference Key Points:
Open Source project: As milestones are reached, code will be released publicly on GitHub.
Inference Compiler: Will allow developers to write Soroban contract specifications. The future intent of the Inference compiler (infc) is to enable automated theorem proving.
Automated Theorem Prover: In the future the infc will allow for automated theorem prover usage. This will allow developers to write Soroban contract specifications and automatically generate proofs, ensuring the contract works according to its specification and the final machine state is reachable.
Documentation and ongoing upkeep: The Inference language is already well documented. The Inference compiler and additional features will receive a similar level of care & maintenance to encourage their use and even beyond.
Different from traditional methods: Traditional methods are effective at proving the presence of bugs, but it can not prove their absence. Inference can.
Directly supports existing Stellar infrastructure: By using Inference, protocols & devs can better prepare themselves for use of the Stellar Audit Bank. This can be streamlined through the process of defining invariants & properties with Inference.
Inference can actually help prepare projects for audits. To prepare for an audit protocols are required to have a clear specification of their protocol’s invariants and assumptions, including edge cases. By writing specifications through Inference, developers can gain additional insights.
To be clear, Inference is a specification engine, not a proving engine. The inference compiler (infc) in its completed state will allow developers to generate complete proofs. The version we are working towards will be a MVP, for which complete proofs are out of scope for this grant. The output from the infc will be .v (proof assistant code) which is a source code file written for an interactive theorem prover, or proof assistant, such as Rocq (formerly Coq). It contains a formal, mathematical representation of a smart contract's logic and the security properties you want to verify, but it would not be completely automated at this stage.
Yes
$149.7K
Our success will be evaluated based on three key areas: technical delivery, community adoption, and ecosystem impact.
MVP (Dec 2025): The inference compiler (infc) can successfully compile .inf files, with open-source code available on GitHub.
Testnet (Feb 2026): Full WASM support, enabling Soroban developers to compile their smart contract specifications into WASM IR.
Mainnet (Apr 2026): Capability to generate Rocq (Coq) theories directly from .inf files, producing valid .v files suitable for proof assistants.
*Note that we use the phrasing of “testnet” & “mainnet” for simplicity to match the tranche guidelines. As a developer tool we do not perform any on-chain transactions.
Growth in the number of Soroban developers actively involved and contributing in Inference development.
Active community engagement through GitHub issues, Discord discussions, and educational material adoption.
Onboarding of security auditors and projects preparing for Stellar audits via Inference specifications.
Increased number of Stellar projects using Inference as part of their audit preparation workflow.
Integration with Stellar developer tooling and recognition by the Stellar community as a standard practice for formal specification.
Measurement: Tracking collaborations with projects, number of audited projects prepared with Inference, and references in Stellar ecosystem reports.
Formal verification has historically been reserved for academic research and security firms, leaving everyday developers without accessible tools to ensure the absence of bugs. With Inference, we are bridging this gap by empowering Stellar developers with a Rust-like formal specification language that integrates directly with Soroban smart contracts.
By delivering open-source tools, engaging directly with developers and auditors, and aligning with Stellar’s long term ecosystem growth, we ensure that security is not an afterthought but an integrated step in their development cycle.
Our mission is simple yet ambitious:
Empower developers with formal verification tooling.
Secure the Stellar ecosystem against critical bugs and vulnerabilities.
For those who made it all the way through our application thank you very much! If you have any comments, questions or feedback (both positive and negative) please let us know directly!
Our go-to-market plan differs a bit from traditional products and services due to the nature of our development tooling. Our main 3 types of users are individual developers, projects that already use Soroban smart contracts, and the security auditors who help keep the other two secure. Each builds upon the other and supports long-term ecosystem security through our open-source software.
Automated Theorem Provers are the most powerful tools to verify code, we want to make it accessible to Soroban developers.
Some other companies build formal verification products for smart contract developers, but what we see is that their solutions are not developer-friendly so these companies operate like security service providers and use their products themselves. We want to build a language that developers will use themselves, and our team will work on improvements.
Developers on Stellar will have access to these tools free of charge in order to help secure the chain, assets, and protect users.
Rust is a commonly used language in the Stellar ecosystem, We will present them with a programming language that is familiar & resembles Rust to already capable developers. If developers know Rust, they can begin using Inference in 20 minutes after reading our documentation.
Similar to how Stellar smart contracts have several characteristics that force contracts to use only a narrow subset of the full Rust language, Inference has similar specifications to keep it secure, simple, and understandable for users of Rust.
Developers will be able to run inference locally on their machines and write specifications easily with a basic understanding of the C language / Rust.
Because Stellar uses a WASM infrastructure, Inference will directly benefit the security of Soroban smart contracts, applications, and the safety of users' assets on Stellar. The use of Inference will directly enable Stellar developers to check the feasibility and vulnerabilities of their code & smart contracts.
Once the Inference compiler reaches a stable version, Soroban developers will be ready to write specifications for Soroban smart contracts themselves. We at Inferara will provide guidance through Stellar-specific documentation and basic integration tutorials. When things are unclear or questions arise, users can reach us directly for support!
With this integration, Stellar smart contract developers will be ready to write formal specifications for Soroban contracts with ease. Inference will be maintained and updated to continually align with Stellar's specifications.
We will engage devs where they hang out:
Access to our open-source code & compiler
Stellar developer discord, webinars, in-person events
Participate & present at weekly Stellar developer meetings (Thursdays). The timezone difference is severe for our team, so bi-weekly is more likely.
Inference initial compiler release showcase & support
Provide existing documentation support & maintenance for Inference
Create educational content to explain complex ideas (Videos, articles, etc.)
Further engage with the community through Discord & other relevant channels
Showcase the differences in our formal verification methods to auditors:
Access to our open-source code & compiler
Provide ecosystem reports of common issues we discover to educate potential users & existing auditors. (the Soroban Security Portal already provides discovered vulnerabilities with semantic search features)
As a team focused on blockchain technology, we will continue to be Stellar advocates both locally and digitally. We are here to stay and since we are heavily focused on formal verification and security, we hope to present the capabilities of Stellar in relevant topic discussions such as zk & privacy technologies.
We are currently still in the research & development phase, however; we have a strong foundation with the inference programming language, which has been well documented as well as a very basic Proof of Concept compiler.
Our current “Playground” POC compiler allows us to emit the ROCQ (Coq) code from the specification. We are applying for this grant in order to build and release a stable version of the Inference compiler, which will take inference code (our programming language), compile it to WebAssembly (WASM with non deterministic extensions as IR (intermediate representation)), and finally translating WASM to V, which is a proof assistant code.
This final result will be computed with our tactics library in order to make sure the final machine state (of the code) is reachable. Essentially, we make sure a smart contract works according to its specification.
Due to the extremely niche scope of our work, we have met with industry experts to assess our research & development goals. One of these researchers is part of the Stellar Research Foundation, who helped us further define our relevance to Stellar. As we are currently focused on developer tooling, we do not currently have many significant KPI such as TVL or other broad values used for on-chain metrics. You can take a look at some of our user general statistics below.
Platform
Users
Twitter / X
67 + 22 in the formal verification space we own (quality over quantity, users)
Telegram (newsletter)
35
Developer Discord
50
575
Medium Article Views
2669
Medium Article Reads
1514
Website visitors:
11,000+
If we can secure development funding, we can divert more of our existing resources towards community development and user acquisition.
We are located & operate in Fukuoka, Japan, which provides us with direct support from the local government to bridge relations with foreign businesses and local talent. We have been actively promoting Stellar via our social media channels as well as hosting an upcoming Stellar event through the Giveth Stellar Community Launch QF Round.
Deliverable: MVP
Brief Description: Inference compiler initial release
How to measure completion:
The inference compiler (infc) repository is open (on GitHub).
infc can compile .inf files.
Estimated date of completion : Dec 20, 2025
Budget : $49,910
Deliverable: Testnet
Brief Description: infc full WASM support
How to measure completion: Infc can emit a valid WASM.
Estimated date of completion : Feb 23, 2026
Budget : $49,910
Deliverable: Mainnet
Brief Description: infc full theory generating support
How to measure completion: infc can compile an arbitrary .inf file and generate a valid Rocq theory (v file).
Estimated date of completion : Apr 20, 2026
Budget : $49,910
We are a small team with a wide range of experiences. Below are our core team members; however, as an open-source project, we have additional students and participants we collaborate with for research & mentorship.
Georgii Plotnikov – founder, MS in computer science, 10+ years of experience in software development, including Web3 development. Github profile
Maxim Savchenko – lead researcher. PhD in mathematics, 15+ years of R&D experience in Formal Methods, Algorithm development, Game theory, and Formal Languages theory.
Dominik Hinkleman - Community Development Lead, Business entrepreneur, BA in Sociology & Psychology, previous grant reviewer & active participant in Web3 governance.
0xGeorgii
Dominik
No other submissions.