(if you would like to view this application in a single document feel free to view it at this link)

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 and correctness proofs in a way that resembles writing unit tests. Inference seeks to bridge the gap between theorem proving and practical application development in blockchains. This approach provides a way to integrate formal verification into the development process of Stellar projects.

Inference Product

1. Inference, a formal specification and verification domain-specific language, was designed for verifying the properties of smart contracts that run on WASM, such as Stellar Soroban.

2. Its syntax is concise and similar to Rust, making it easy for Soroban developers to use.

3. By writing formal specifications in a way that resembles writing unit tests, Stellar protocol developers can bridge the gap between theorem proving and practical application development in blockchains,  ensuring that Stellar smart contracts are secure and reliable.

4. This approach integrates formal verification into the development process of Stellar projects.

**Inference Key Points:

**

Open Source project

**As milestones are reached for stable versions, code will be released publicly on github

**

Inference Compiler

Will allow developers to write Soroban contract specifications

Automated Theorem Prover

The Automated Theorem Prover feature 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 on-going upkeep**

The inference language is already well documented. The Inference compiler and additional features will receive a similar level of care & maintenance to encourage its use.

We will divide success criteria into these categories: 

1. Tool usage & Awareness

2. Ecosystem Security

3. Community Engagement

Tool usage & Awareness -

**Having relevant parties using our tools through use of the created documentation, educational materials and the Inferara teams active participation in relevant communities.

Ecosystem Security-

Although we can not guarantee that we will find a critical bug in existing code, if developers or projects discover potential issues before release it will be a win for everyone involved. By flagging and understanding potential issues, we can secure Stellar even further.**

Community Engagement- 

**Receiving valuable feedback from developers, users and Stellar projects is crucial.
We want to build a tool that will be used, improved and help prevent critical errors, not another impractical tool that goes unused.
**

**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.

Individual Developers**

**Automated Theorem Provers are the most powerful tools to verify code, we want to make it accessible to 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 mostly operate like security service providers and use their products themselves. Our goal is the opposite; 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 a programming language that is familiar & resembles Rust to already capable developers.

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 C language / Rust

Because Stellar uses a WASM infrastructure, Inference will directly benefit the security of Soroban smart contracts, applications and 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, Stellar 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.

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.**

**Developer Outreach:
We will engage devs where they hang out

**

• Access to our open source code & compiler

• **Stellar developer discord, webinars, in person events
  (Primarily in Japan but not limited to)**

• Participate & present at weekly Stellar developer meetings (Thursdays). The time zone 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

  **

**Stellar Community Projects:

This section focuses primarily on Stellar ecosystem projects, but is not limited to them.** 

We understand that audit credits are provided for projects & teams that work through the SCF process through the Audit Bank**. We hope to be an additional yet, different approach to verifying the security of code written for Soroban.
**

Strategic Partnerships:

• Re-evaluate existing projects code for pro-active bug finding

• Identify relevant SCF projects to support

• Identify and contact other existing stellar projects

• Provide consultation & guidance to projects

**
Note: A correctness certificate Inference compiler generates is an unambiguous, irrefutable evidence that guarantees that formally defined properties are truly held.**

**
Security auditors can use Inference to model attack vectors and use the information to suggest changes in code**

Security Auditors:

• 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 in order to educate potential users & existing auditors

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 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 compiler Inference compilation process consisting of taking inference code (our programming language), compiling to WebAssembly (WASM), and finally translating WASM to V which is proof assistant code.

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, Giuliano Losa 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.

You can take a look at some of our user statistics below.

Twitter / X: 36 + 18 in the formal verification space we own (quality over quantity users)**

Telegram: 37

Developer Discord: 25

LinkedIn: 370

GitHub: 5

**website visitors: 11,000

If we are able to 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 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.