Examples

Working bmc4j projects you can clone, read, and run — every @BmcProof in them is checked by the engine, not just illustrative.

Feature modules

Example modules (bmc4j repo) Topic-organised @BmcProof modules — fundamentals, language features, the standard library, contracts, and integrations. The guided tour of what bmc4j can do.

Real algorithms

TheAlgorithms — Java bmc4j proofs over vendored TheAlgorithms/Java sources — proving (and refuting) real algorithm implementations.

TheAlgorithms — Kotlin The same, over vendored TheAlgorithms/Kotlin algorithms.

Real-world code

kotlinx.collections.immutable Proving a third-party Kotlin library's functions as shipped — no source changes, just the published artifact.

Full domain example A complete domain model proved end-to-end with bmc4j.