The Soroban Disassembler is an open-source specialized decompilation tool that can receive the WASM file of a Soroban Smart contract and output easily readable WAT and relevant Rust code. It seeks to create a higher level of accuracy than existing WASM -> WAT conversion tools. 

As this proposal is for the Soroban Specialized Reverse Engineering Tool RFP, it will abide by the expected deliverables requested.
These are detailed further in the Technical Architecture document

$100.0K

Our team at Inferara is an independent research group founded to bridge the gap between Formal Methods and mainstream engineering. Our abilities are demonstrated through past experience as individuals and what we have delivered as a team. As a team we published the comprehensive Inference Language Specification (built for WASM), documentation, also research articles and blog posts which further explore the importance of byte-code level verification. There is also ongoing research into non-deterministic computations. We have a strong combination of academic and hard skills which we apply to our work.

Team collaborative achievements:

• We understand the detailed internals of WASM and have applied that knowledge, you can see some of our existing tools here

• We have written extensively about WASM:

  • https://inferara.com/blog/preparing-polkadot-pallet-balances-for-formal-verification/

  • https://inferara.com/blog/new-approach-to-formal-verification-smart-contracts/

  • https://inferara.com/blog/monolithic-architecture-vs-fv/

• We have built the Soroban Security Portal database and will use it to get additional test cases (Soroban contracts)

Individual Team Members & Achievements

• Maxim Savchenko - expert in WASM and its computation model.

  • Researcher since 2005

  • Extensive research into WASM systems. 

  • Preparing Polkadot pallet Balances for Formal Verification

  • Influence of additional information asymmetry on the solutions of non-antagonistic games, PhD

  • MS Algorithmic Languages

• Yoshihiro Imai - Proof Ninja, extensive WASM experience

  • Extensive experience in language specifications, web3 and WASM.

  • Works closely with WASM modules and inference programming language specification. 

  • Relevant Publications:

    • Types and Programming Languages (Japanese Edition)

    • 入門OCaml ~プログラミング基礎と実践理解

  • Master of Mathematics (March 2007, Nagoya University)

  • Further experience can be seen here

• Dominik Hinkleman

  • 9 years of blockchain experience both as a user, active governance delegate and community builder. 

  • Created grant framework and standards for the grant review process for the PoolTogether DAO.

  • Performed Discord wizardry for ChoiceDAO, which helped raise $20k in donations

  • Maintainer of vulnerabilities and information for Soroban Security Portal. 

  • Sociology BS (Tennessee Tech University, 2017)

As this submission is to fill the RFP from the Stellar Foundation we do not have any traction to show for this project at this time. Below are some details from our initial interest form submission:

Inferara has been operating for 2 years and building on Stellar since summer of 2025. As a R&D team we build custom solutions and research services. Our tools identify conflicts of logic in code. We do this by making the power of formal verification directly accessible to developers without requiring a PhD in mathematics.

Through SCF we have built inference, a formal specification & verification language. It focuses on the emission of WASM from a specification. For this project creating a reverse engineering tool that produces WAT from WASM is extremely relevant to our expertise.

We have also built the Soroban Security Portal, a knowledge base that provides detailed information from audit reports of Stellar projects. We manually log details from each submitted vulnerability and provide additional context. It is still actively maintained.

The first tranche will be focused on establishing the proper framework and foundation of the project. This includes the beginning of WASM parsing + spec extraction. A basic implementation of CLI, library as well as preparing meaningful ways to measure the performance of Soroban Decompiler.

How to measure completion:

• The project is set up and well organized (CI, documentation, crate structure, etc.)

• Library skeleton in place

• CLI skeleton in place

• Implemented WASM parser module 

• Simple Spec extraction process is available

• Can produce basic TypeRegistry from Soroban WASM files

Budget: $20,000

During tranche 2 we intend to be able to partially decompile contracts (simple arithmetic, basic storage, custom types, auth, cross-contract, events) with proper reconstruction to compilable Rust with correct types and signatures.

How to measure completion:

• Capable of partial decompilation of contracts such as (simple arithmetic, basic storage, custom types, auth and cross-contract events) to Rust. Includes correct types and signatures. 

Budget:

$30,000

Tranche 3 will provide the completed full production ready version for developers or anyone to use the Soroban Disassembler to take Soroban contract data and receive both readable WAT and corresponding Rust code. The open-source release will also include detailed documentation, published crates and CI/CD pipeline. This combination of tools ensure that testing criteria as stated in the RFP is met.  Including a comprehensive testing suite.

How to measure completion:

• The accuracy framework allows for 90%+ overall accuracy across SDK test contracts

• Test suite: CI green, regression detection working 

• Production of human-readable reports

• Functional equivalence tests: compile decompiled code back to WASM, run through soroban-env-host, compare outputs against original. 

• ~95%+ compilation success, ~90%+ behavioral match

• Public documentation available

• Download deployed Soroban contracts from mainnet. Run the decompiler.
  Validate: compiles, spec-consistent, structurally plausible

• Soroban-decompiler (Library) and soroban-decompile (CLI) are publicly available through crates.io

  Budget: $40,000

Our team at Inferara is an independent research group founded to bridge the gap between Formal Methods and mainstream engineering. Our abilities are demonstrated through past experience as individuals and what we have delivered as a team. As a team we published the comprehensive Inference Language Specification (built for WASM), documentation, also research articles and blog posts which further explore the importance of byte-code level verification. There is also ongoing research into non-deterministic computations. We have a strong combination of academic and hard skills which we apply to our work. 

Maxim Savchenko

Researcher since 2005

Extensive research into WASM systems.
Preparing Polkadot pallet Balances for Formal Verification

Influence of additional information asymmetry on the solutions of non-antagonistic games, PhD

MS Algorithmic Languages

Yoshihiro Imai
Works closely with WASM modules and inference programming language specification. Extensive experience in language specifications, web3 and WASM.

Master of Mathematics (March 2007, Nagoya University)

Relevant Publications:
Types and Programming Languages (Japanese Edition)
入門OCaml ~プログラミング基礎と実践理解

Additional details can be found here

Xuanrui Qi 

Writing code since 2014

Developing in Web3 since 2020

Academic experience in formal methods & programming language design

Ph.D. MS in Mathematical Science

Type theory and the logic of toposes

MS in Computer Science from Nagoya University

Dominik Hinkleman

9 years of blockchain experience both as a user, active governance delegate and community builder. 

Maintainer of vulnerabilities and information for Soroban Security Portal. 

Sociology BS (Tennessee Tech University, 2017)