AI Formal Verification tool for JAM

Tech Talk
1

Hello, my name is Georgii, and I’ve been participating in Polkadot for some time now. Our team at Inferara has been developing the open-source Inference programming language and its supporting compiler. It’s intended to make the power of formal verification accessible to developers without requiring a PhD in mathematics.

In order to make it more accessible to developers, we are exploring the idea of creating a coding agent tool that will use formal verification enhance the quality of code.

As we’ve seen, Polkadot is moving to support products over ideas. We need real products and dapps that people will use. We want to hear some feedback on this product idea and if it could get devs interested and ready for JAM.

There should be as many people building and experimenting with building on Polkadot, and with our tool, they can be productive without sacrificing safety.

But the issue is that if pallet-revive & RISC-V aims to make Polkadot language agnostic (can use Solidity, C, Rust, etc.), it means the potential errors landscape expands for the number of SDKs provided accordingly. Which makes things more difficult to learn, track, and mitigate. Here, Inference acts as a baseline of the security/implementation correctness.

Individuals and small dev teams often struggle with funding, time, and sometimes tricky security experience (therefore, audit firms exist). Due to those circumstances, teams rely on AI assistance, which cannot guarantee the code is safe.

There needs to be a pragmatic way to ensure code intention & outcomes from potentially sloppy LLM code adhere to smart contract standards & business logic.

When using Inference as part of the dev process for those who already use AI agents, it adds an extra level of implementation accuracy for code.

We combine the speed of AI agents like Claude and Codex with the power of formal methods to make fast-paced development safer and without being jammed.

By adding some additional implementation checks for vibe coders, we invite curious builders who might not be experts (yet), by making Polkadot accessible to new devs while easing learning curves and reducing sloppy code.

We would do this by pairing a coding agent with a mathematical safety net where:

  1. You define the constraints (the Spec) for your logic.
  2. Developers (or agents) handle implementation.
  3. Inference verifies implementation is mathematically sound.

As this is just an idea for open discussion, please share any feedback.
There are also some questions below to get some discussions started.

Questions

  1. As we anticipate JAM, would a tool that fact-checks AI-generated work be useful?
  2. Would the idea of AI + Formal Verification get developers interested in Polkadot?
  3. Is there any interest in the Inference programming language?
4 Likes
2

+1 for Georgii, nice guy that has been around the ecosystems for several years

I think more testing and quality assurance should be a net benefit, But, since I am not a Jam implementor/dev maybe its better to poke some of the Jam implementors(JAM Gray Paper) ?

Questions:

  • 1 - “exploring the idea of creating a coding agent tool that will use formal verification enhance the quality of code“ - Which LLM models/coding agents will you guys use or plan?
  • 2 - As a developer doing smart contracts can I use inference today ?
  • 3 - Who is the target group ? is it solidity developers ? is it rust developers that want to hack together polkavm contracts? Could I use inference with rust + polkavm, for this repo KusamaShield/PoseidonPolkaVM: Poseidon hashing for Polkavm with solidity compatibility - Codeberg.org ?
  • 4 - Is there any PoC of smart contracts or wasm code that use Inference for their testing suit?
  • 5 - Is risc-v and polkavm on the roadmap?

Thanks

~flipchan

1 Like
3

1 - “exploring the idea of creating a coding agent tool that will use formal verification enhance the quality of code“ - Which LLM models/coding agents will you guys use or plan?

The first version of the Inference skill is not based on LLM at all. This is planned to be used for coding agents, whichever you prefer, that is most relevant to your needs. Common ones we anticipate using our skill would be Claude Code, Codex, and Gemini CLI.

2 - As a developer doing smart contracts can I use inference today ?

We plan on having a stable version release in April-May of this year with more robust features and uses in the summer. For now, you can see our progress and updates (here)[GitHub - Inferara/inference: 🌀 Inference programming language] as well as the usual socials from the homepage.

However, the coding agent skill will be available by March. It will use the latest Inference features as soon as they are available, but will be useful from day one.

3 - Who is the target group ? is it solidity developers ? is it rust developers that want to hack together polkavm contracts? Could I use inference with rust + polkavm, for this repo KusamaShield/PoseidonPolkaVM: Poseidon hashing for Polkavm with solidity compatibility - Codeberg.org ?

In the first iteration Inference is meant to be used more for sdk’s, cryptographic, and zk primitives, libraries; the second iteration would be more suited for smart contract development. The Inference AI skill is useful for smart contract development perfectly because it applies the methods of Inference to the code being produced by agents.

4 - Is there any PoC of smart contracts or wasm code that use Inference for their testing suit

Not at this time, but we have done some research on exploring the application of formal verification on Polkadot runtime (here)[pallet-balances-formal-verification/preparation/preparing-polkadot-pallet-balances-for-formal-verification.md at 0e4b1527e0d2796d7d241dd2ad4934f7924ed4bb · Inferara/pallet-balances-formal-verification · GitHub]

5 - Is risc-v and polkavm on the roadmap?

risc-v is on our minds for future implementation.

4

what you are building is pretty ground breaking, and since meeting in Sub0 bangkok, i have learned from the work you do about how to think about designing systems prioritising formal verification in the pursuit of the provable resilience of the system being built.

And afaiu, what you are building is a language that is constrained to only allow for a specific way of coding, and a compiler that checks it for formal verification using theorem proofs. so this is not your normal general low level programming language.

i particular learned from your post, which is an analysis of Polkadot, stellar and arbitrum from the perspective of how well it is designed for formal verification. In Polkadot, i see that on the face of it, it would appear with the pallets being modular that it is designed for correctness . but after compilation the runtime become one large interwoven monolith, which makes it impossible to prove correctness of any specific function.

At the JAM protocol level, which has the JAM prize i am participating in, i believe that the formulas in the graypaper are designed with correctness backed up by theorem proofs. However on the implementation side, it’s unlikely there is any single implementation that is thinking to code for the level of formal verification you are talking about. simply because that language/compiler doesn’t exist yet if am not mistaken?

It is definitely worth exploring further with W3F and @gavofyork

1 Like
5

Let me share a few thoughts on this regard. Fundamentally, what does it mean for a theorem to be “proven”? Traditionally, it means a proof exists that has been meticulously scrutinized by humans (ideally multiple independent reviewers or teams of reviewers) using a pen and paper approach to confirm:

  1. The proof is integrity correct
  2. The proof actually proves what is needed
  3. There are no contradictions in the proof or the theory.

A good practice here is to explicitly demonstrate which counterexample vectors were considered and why they are unsustainable.

Alternatively, for complex proofs, theorem provers are used to mathematically certify that the steps inevitably lead to the correct conclusion. It works because of the nature of how theorem provers work. De facto, they are lexical type checkers. But, the magic is that the strict type system forces correctness; for reference, see CIC.

Simply saying, we can type-check that the proof is constructed properly. It means that it uses only allowed logic-flow transformation. And it absolutely bans any sort of intrusive assumptions, so that you can use someting IIF its definition already exists.

With a bit zoomed out view, under the Curry–Howard correspondence, a proof effectively becomes a function for a given input (propositions as types, proofs as programs). And this actually leads me to a fascinating convergence.

Inference source code embeds the formal specification directly. Actually, any Inference code, even outside of the specification (for execution), becomes part of the formal specification of the given program. This means Inference is simultaneously program code (execution semantics) and a proof (higher-order logic semantics). When you write Inference code for your algorithm, you are writing the proof of that algorithm’s behavior at the same time. Like reverse Curry-Howard correspondence.

3 Likes