Andy Kaufman

<img src="https://giveth.mypinata.cloud/ipfs/QmbXzU61L8pKY4y2nED6PC69a2hf93zRfNsNPPie1yKsjn" /><a href="https://github.com/Inferara/inference" rel="noopener noreferrer" target="_blank">Inference</a> is a programming language with built in formal verification capabilities, designed for critical and high assurance systems development. With it you can write mathematically verified correct code without a PhD in math. In our web3 world when there is an error in smart contract code it can cause millions to be lost. While formal verification is the gold standard for security, it has historically been reserved for aerospace, military, and academic circles due to its complexity. We plan to change this with the use of Inference, which is a programming language where security is part of the design instead of being an afterthought for future audits. Our goal is to bring the power of mathematical proof assistants (like Rocq/Coq) into a familiar, Rust-like environment, allowing every developer to write code that is mathematically guaranteed to behave as intended. Inference breakdownInference is both an executable programming language and a formal specification language.<ul><li>Accessible Formal Methods: You don't need to be a mathematician to use Inference. We use high-level abstractions like "forall", "exists", and "assume" to let you define logic that the compiler verifies automatically.</li><li>Built for Web3: By targeting WebAssembly (WASM), Inference is designed for the modern decentralized web, L2 execution environments, and mission-critical robotics/AI systems.</li><li>The concept of Uzumaki: (pronounced u-zu-ma-ki 🌀) acts like a digital whirlpool that splits a single execution path into every possible scenario simultaneously. Instead of testing just one specific input, it allows the compiler to evaluate every value a variable could potentially hold all at once. While traditional testing only proves that specific bugs exist, Uzumaki enables Inference to mathematically prove the absence of bugs by verifying that the code remains correct across every possible computational branch.</li></ul> Project statusThe Inference project started in January 2023. It is open source and we have been actively developing it. There are several components closely intertwined that are actively being developed and improved:<ul><li>Language Specification: A comprehensive <a href="https://github.com/Inferara/inference-language-spec" rel="noopener noreferrer" target="_blank">specification</a> defining our deterministic computing model.</li><li>Inference Compiler (infc) <a href="https://github.com/Inferara/inference" rel="noopener noreferrer" target="_blank">v0.0.1-alpha</a>: First release.</li><li>can compile .inf into WASM</li><li>Formal Logic Backend: Preliminary work on translating code into V (Proof Assistant code) to interface with the Rocq (Coq) theory prover.</li><li>mac / windows / linux support </li></ul> We aim to combine the reliability and speed of the Rust programming language and the Rocq theory prover. Our plansYour contributions directly fund the open-source development of the Inference tools.Our next phase of development includes:<ol><li>WASM-to-V Translator: Completing the bridge between executable WASM and machine-checked proofs.</li><li>EVM Compatibility: Extending our backend to support Ethereum Virtual Machine capabilities, allowing Inference to be used for secure smart contract development.</li><li>Capability to generate Rocq (Coq) theories directly from .inf files, producing valid .v files suitable for proof assistants</li><li>Future Developer Tooling: LSP support for VS Code to provide real-time logic checking as you type.</li></ol> Why is this a public good?We believe that security should not be a luxury. By supporting Inference, you are helping build an open-source infrastructure that:<ul><li>Reduces the frequency and impact of smart contract exploits.</li><li>Lowers the barrier of entry for high security development.</li><li>Ensures that as we move toward AI-managed systems and robotics, the underlying software is provably safe.</li></ul>Ways to contribute<ul><li>Donate: any amount is appreciated.</li><li>Star our Repo: at<a href="https://github.com/Inferara/inference" rel="noopener noreferrer" target="_blank"> https://github.com/Inferara/inference</a>.</li><li>Read &amp; the Guide: Inference Book at<a href="https://inference-lang.org/book" rel="noopener noreferrer" target="_blank"> https://inference-lang.org/book</a> and give us feedback.</li><li>Join the Research: We are an independent research group. If you are passionate about formal methods, let's build the future together. We can be reached through the socials provided. </li></ul> Extra links<ul><li>Website:<a href="https://www.inferara.com/en/" rel="noopener noreferrer" target="_blank"> </a><a href="https://www.inferara.com/en" rel="noopener noreferrer" target="_blank">https://www.inferara.com/en/</a></li><li>Compiler Repo:<a href="https://github.com/Inferara/inference" rel="noopener noreferrer" target="_blank"> https://github.com/Inferara/inference</a></li><li>Documentation:<a href="https://inference-lang.org/book" rel="noopener noreferrer" target="_blank"> https://inference-lang.org/book</a></li></ul>

Securing web3 with the Inference Programming Language
Andy Kaufman

Donate first & lead the way!

Securing web3 with the Inference Programming LanguageAndy Kaufman

Donate first & lead the way!

Securing web3 with the Inference Programming Language
Andy Kaufman