Inference v0.0.6 ships Stellar as a compilation target, enabling developers to use the formal verification language to write and prove Soroban smart contracts. The release also adds SpaceWasm target support for NASA JPL flight software and improves proof generation with Rocq.
Inference v0.0.6 introduces Stellar as a compilation target, allowing developers to write formally verified Soroban smart contracts in Inference and deploy them directly to the network. The new `--target stellar` command generates Soroban-compatible smart contracts complete with contractspec and contractmeta sections, enabling type-aware contract interaction through stellar-cli and binding generators. Beyond Stellar, the release ships SpaceWasm target support for NASA JPL's flight interpreter, enabling embedded systems and aerospace software verification. Proof verification via Rocq is significantly strengthened with a new IR foundation, support for existential and uniquely-quantified specification functions, and multiple soundness improvements. The release includes extensive breaking changes to language semantics reflecting the language's evolution toward production-ready formal verification for smart contracts.
