{"article":{"slug":"creusot-0-14-0","title":"Creusot 0.14.0","subtitle":null,"summary":"The Creusot team announces version 0.14.0 of their formal verification tool for Rust, highlighting selected new features for contracts and proofs and pointing to the full changelog for the release.","content_type":"changelog","language":"en","canonical_url":"https://devlog.creusot.rs/v0-14-0/","author":{"name":null,"url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"Creusot","url":"https://creusot.rs/","listing_slug":null,"listing":null},"topics":[{"name":"Rust","slug":"rust","url":"https://listedarticles.com/topics/rust"},{"name":"Programming","slug":"programming","url":"https://listedarticles.com/topics/programming"},{"name":"Open Source","slug":"open-source","url":"https://listedarticles.com/topics/open-source"},{"name":"Developer Tools","slug":"developer-tools","url":"https://listedarticles.com/topics/developer-tools"},{"name":"Software Engineering","slug":"software-engineering","url":"https://listedarticles.com/topics/software-engineering"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":983,"reading_minutes":4,"published_at":"2026-10-13T00:00:00.000Z","added_at":"2026-10-13T08:13:56.727Z","updated_at":"2026-10-13T08:13:56.727Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/creusot-0-14-0","markdown_url":"https://listedarticles.com/articles/creusot-0-14-0.md","example":false,"citation":"Creusot. \"Creusot 0.14.0.\" 13 Oct 2026. https://devlog.creusot.rs/v0-14-0/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://devlog.creusot.rs/v0-14-0/"},"body_markdown":"# Creusot 0.14.0\n\n2026-10-13\n·\n5min\n\nWe are pleased to announce the release of version 0.14.0 of [Creusot](https://creusot.rs),\nour formal verification tool for Rust.\n\nIn this post, we highlight a small selection of new features.\nSee the full [changelog](https://github.com/creusot-rs/creusot/blob/master/CHANGELOG.md#0140---2026-10-09)\nfor the rest.\n\n# What's new in Creusot?\n\n## Partial orders\n\nPreviously, Creusot restricted its specification of `PartialOrd` to total\norders. Since version 0.13.0, we have relaxed it to allow partial orders.\n(We skipped a devlog entry for 0.13.0 so let's talk about this here.)\n\nOur previous definition of total order (`OrdLogic`) relied on the\ncomparison function `cmp_log` (the logic counterpart to `cmp`), which returns an `Ordering`.\n\n```\n// Old definition of total order\npub trait OrdLogic {\n #[logic]\n fn cmp_log(self, other: Self) -> Ordering;\n\n // ... (laws and other comparison operators)\n}\n```\n\nThat had the benefit of making totality an implicit consequence of the type of the function:\nany two elements must compare either `Less` , `Equal`, or `Greater`.\n\nWith the switch to partial orders, a traditional formulation based on a\nboolean comparison function (\"`<`\", aka. `lt_log`) becomes more natural.\nA strict partial order (`PartialOrdLogic`) consists of a comparison function `lt_log` which\nis irreflexive and transitive. Totality becomes another law: for all `x`, `y`,\nthe trijunction `x < y || x == y || y < x` must hold.\n\n```\n// (New) definition of partial order\npub trait PartialOrdLogic {\n /// `self < other` in logic\n #[logic]\n fn lt_log(self, other: Self) -> bool;\n\n // ... (laws (irreflexivity, transitivity) and other comparison operators)\n}\n\n// New definition of total order\npub trait OrdLogic {\n /// The order is total\n #[logic(law)]\n #[ensures(self < other || self == other || other < self)]\n fn lt_log_total(self, other: Self);\n}\n```\n\nInterestingly, none of our existing proofs were affected by this change.\nOur automated provers just took it in stride.\n\n## Logic VC gen\n\nCreusot now generates verification conditions (VCs) for snapshots,\nwhich are logic expressions embedded in Rust programs.\nIn particular, this enhances the use of \"lemma functions\",\na common idiom in verification tools similar to Creusot.\n\nFor example, you can encode a lemma as a logic function such as this,\nwhich logically amounts to the proposition `forall hyp(x) -> concl(x)`:\n\n```\n#[logic]\n#[requires(hyp(x))]\n#[ensures(concl(x))]\nfn lemma(x: usize) {}\n```\n\nThen, inside a program function you can call `lemma` inside a `snapshot!`:\n\n```\nfn f(n: usize) {\n snapshot!(lemma(n));\n}\n```\n\nCreusot now translates this call to an assertion that `hyp(n)` (the precondition of `lemma`) is true\nand an assumption that `concl(n)` (its postcondition) is true. Notably, these statements\nare specialized to `n`, the argument of `lemma`, so we avoid relying on provers to\ninstantiate the universal quantifier in `forall hyp(x) -> concl(x)`.\n\nIt should be said that this new feature specifically enables *logic* functions to be\nused as lemma functions.\nBefore, you could already do something similar with program functions:\n\n```\n#[requires(hyp(x))]\n#[ensures(concl(x))]\nfn lemma(x: usize) {}\n\nfn f(n: usize) {\n lemma(n);\n}\n```\n\nThe difference is that (1) this version introduces a Rust function call, however\ntrivial it may be, and (2) it must pass the borrow checker, which may require\nboilerplate to work around when all you wanted is to state some facts.\nIn contrast, snapshots are entirely erased, so it is clear that\nthey are there only for the sake of formal proof.\nThus, these newly generated VCs for snapshots let us draw clearer boundaries\nbetween the worlds of programs and proofs.\n\nIt may seem surprising that Creusot did not already do this. This comes down to\nthe fact that programs and specifications are written in two separate languages,\nwith their own semantics, and thus with different mechanisms and motivations for generating VCs.\nWithout going into too much details, VCs were originally not generated for `snapshot!`\nbecause it isn't necessary for soundness, but it turns out to help catch mistakes\nin specifications quicker (such as out-of-bounds indexing), on top of enabling\nnew techniques such as that described above.\n\n## rust-analyzer integration\n\nIt is finally possible to use Go-to-definition in Pearlite specifications.\n\n![Screenshot of go-to-definition working in the middle of a Creusot specification](https://devlog.creusot.rs/creusot-go-to-definition.png)\n\nTo start, we needed to make rust-analyzer expand the code of specifications.\nIn normal compilation, specification macros (`#[requires]`, `#[ensures]`,\n`proof_assert!`, `snapshot!`, etc.) erase themselves, discarding their contents.\nWe just needed to pass options to rust-analyzer for it to expand those macros the same way Creusot does\n(see [our guide for the relevant rust-analyzer settings](https://guide.creusot.rs/quickstart/editor_config.html)).\n\nOne worry we had was that Pearlite macros expand to not quite valid Rust code,\nnot meant to be compiled by rustc:\nit passes the type checker, but not the borrow checker.\nLuckily for us, rust-analyzer does not do borrow checking,\nso it doesn't see any problem with the expanded code.\n\nWith that done, Go-to-definition did start to work, but it returned numerous irrelevant results.\nThe problem was that the tokens produced by Pearlite macros carried spans that were\ntoo coarse-grained.\n\nTo explain it very roughly, when you activate Go-to-definition,\nrust-analyzer looks for identifiers in the final AST whose span ranges over your cursor.\nFor example, `a + b` in Pearlite expands to a method call\n`::creusot_std::logic::ops::AddLogic::add_logic(a, b)`,\nwhere every generated token carries the span of the whole expression `a + b`.\nHence, Go-to-definition from anywhere in that expression ends up looking up the definitions\nof all of `creusot_std`, `logic`, `ops`, `AddLogic`, and `add_logic`.\n\nIn this case, we'd like to only look up `add_logic`, and only when the cursor is right next to `+`.\nThe fix is to make the token `add_logic` have the span of `+`, and\nto make the other identifiers have a zero-width span,\nwhich seems to be enough for rust-analyzer to ignore them.\n\nMany thanks to Sarah Quiñones for figuring all this out.\nThis fix makes navigating specifications in Creusot much more pleasant.\n\n---\n\nThanks for tuning in. If you have any questions about Creusot, you are welcome to join\n[our Zulip channel](https://why3.zulipchat.com/#narrow/channel/341707-creusot),\nor to open a [discussion](https://github.com/creusot-rs/creusot/discussions)\nor an [issue](https://github.com/creusot-rs/creusot/issues) on the Creusot repository.\n\n---\n","body_html":"

Creusot 0.14.0

\n

2026-10-13\n·\n5min

\n

We are pleased to announce the release of version 0.14.0 of Creusot,\nour formal verification tool for Rust.

\n

In this post, we highlight a small selection of new features.\nSee the full changelog\nfor the rest.

\n

What's new in Creusot?

\n

Partial orders

\n

Previously, Creusot restricted its specification of PartialOrd to total\norders. Since version 0.13.0, we have relaxed it to allow partial orders.\n(We skipped a devlog entry for 0.13.0 so let's talk about this here.)

\n

Our previous definition of total order (OrdLogic) relied on the\ncomparison function cmp_log (the logic counterpart to cmp), which returns an Ordering.

\n
// Old definition of total order\npub trait OrdLogic {\n    #[logic]\n    fn cmp_log(self, other: Self) -> Ordering;\n\n    // ... (laws and other comparison operators)\n}
\n

That had the benefit of making totality an implicit consequence of the type of the function:\nany two elements must compare either Less , Equal, or Greater.

\n

With the switch to partial orders, a traditional formulation based on a\nboolean comparison function ("<", aka. lt_log) becomes more natural.\nA strict partial order (PartialOrdLogic) consists of a comparison function lt_log which\nis irreflexive and transitive. Totality becomes another law: for all x, y,\nthe trijunction x < y || x == y || y < x must hold.

\n
// (New) definition of partial order\npub trait PartialOrdLogic {\n    /// `self < other` in logic\n    #[logic]\n    fn lt_log(self, other: Self) -> bool;\n\n    // ... (laws (irreflexivity, transitivity) and other comparison operators)\n}\n\n// New definition of total order\npub trait OrdLogic {\n    /// The order is total\n    #[logic(law)]\n    #[ensures(self < other || self == other || other < self)]\n    fn lt_log_total(self, other: Self);\n}
\n

Interestingly, none of our existing proofs were affected by this change.\nOur automated provers just took it in stride.

\n

Logic VC gen

\n

Creusot now generates verification conditions (VCs) for snapshots,\nwhich are logic expressions embedded in Rust programs.\nIn particular, this enhances the use of "lemma functions",\na common idiom in verification tools similar to Creusot.

\n

For example, you can encode a lemma as a logic function such as this,\nwhich logically amounts to the proposition forall<x> hyp(x) -> concl(x):

\n
#[logic]\n#[requires(hyp(x))]\n#[ensures(concl(x))]\nfn lemma(x: usize) {}
\n

Then, inside a program function you can call lemma inside a snapshot!:

\n
fn f(n: usize) {\n   snapshot!(lemma(n));\n}
\n

Creusot now translates this call to an assertion that hyp(n) (the precondition of lemma) is true\nand an assumption that concl(n) (its postcondition) is true. Notably, these statements\nare specialized to n, the argument of lemma, so we avoid relying on provers to\ninstantiate the universal quantifier in forall<x> hyp(x) -> concl(x).

\n

It should be said that this new feature specifically enables logic functions to be\nused as lemma functions.\nBefore, you could already do something similar with program functions:

\n
#[requires(hyp(x))]\n#[ensures(concl(x))]\nfn lemma(x: usize) {}\n\nfn f(n: usize) {\n    lemma(n);\n}
\n

The difference is that (1) this version introduces a Rust function call, however\ntrivial it may be, and (2) it must pass the borrow checker, which may require\nboilerplate to work around when all you wanted is to state some facts.\nIn contrast, snapshots are entirely erased, so it is clear that\nthey are there only for the sake of formal proof.\nThus, these newly generated VCs for snapshots let us draw clearer boundaries\nbetween the worlds of programs and proofs.

\n

It may seem surprising that Creusot did not already do this. This comes down to\nthe fact that programs and specifications are written in two separate languages,\nwith their own semantics, and thus with different mechanisms and motivations for generating VCs.\nWithout going into too much details, VCs were originally not generated for snapshot!\nbecause it isn't necessary for soundness, but it turns out to help catch mistakes\nin specifications quicker (such as out-of-bounds indexing), on top of enabling\nnew techniques such as that described above.

\n

rust-analyzer integration

\n

It is finally possible to use Go-to-definition in Pearlite specifications.

\n
\"Screenshot
\n

To start, we needed to make rust-analyzer expand the code of specifications.\nIn normal compilation, specification macros (#[requires], #[ensures],\nproof_assert!, snapshot!, etc.) erase themselves, discarding their contents.\nWe just needed to pass options to rust-analyzer for it to expand those macros the same way Creusot does\n(see our guide for the relevant rust-analyzer settings).

\n

One worry we had was that Pearlite macros expand to not quite valid Rust code,\nnot meant to be compiled by rustc:\nit passes the type checker, but not the borrow checker.\nLuckily for us, rust-analyzer does not do borrow checking,\nso it doesn't see any problem with the expanded code.

\n

With that done, Go-to-definition did start to work, but it returned numerous irrelevant results.\nThe problem was that the tokens produced by Pearlite macros carried spans that were\ntoo coarse-grained.

\n

To explain it very roughly, when you activate Go-to-definition,\nrust-analyzer looks for identifiers in the final AST whose span ranges over your cursor.\nFor example, a + b in Pearlite expands to a method call\n::creusot_std::logic::ops::AddLogic::add_logic(a, b),\nwhere every generated token carries the span of the whole expression a + b.\nHence, Go-to-definition from anywhere in that expression ends up looking up the definitions\nof all of creusot_std, logic, ops, AddLogic, and add_logic.

\n

In this case, we'd like to only look up add_logic, and only when the cursor is right next to +.\nThe fix is to make the token add_logic have the span of +, and\nto make the other identifiers have a zero-width span,\nwhich seems to be enough for rust-analyzer to ignore them.

\n

Many thanks to Sarah Quiñones for figuring all this out.\nThis fix makes navigating specifications in Creusot much more pleasant.

\n
\n

Thanks for tuning in. If you have any questions about Creusot, you are welcome to join\nour Zulip channel,\nor to open a discussion\nor an issue on the Creusot repository.

\n
","headings":[{"level":1,"text":"Creusot 0.14.0","id":"creusot-0-14-0"},{"level":1,"text":"What's new in Creusot?","id":"what-s-new-in-creusot"},{"level":2,"text":"Partial orders","id":"partial-orders"},{"level":2,"text":"Logic VC gen","id":"logic-vc-gen"},{"level":2,"text":"rust-analyzer integration","id":"rust-analyzer-integration"}]}}