Skip to content

Conversation

@yoav-el-certora
Copy link
Contributor

No description provided.

johspaeth and others added 22 commits June 30, 2025 09:15
* 7.26.0 Release (#163)

* Niv/cert 8248 revert example (#155)

* CERT 8248 Add Revert Example

* Update README

* Address Christiane review

* Update example based on Nurit Review

* Clean

* Update config.yml (#160)

Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>

* Example ready

* christiane cr

* Code reviews

---------

Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com>
Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com>
Co-authored-by: liav-certora <liav@certora.com>

* Bug fixed

* Add an example on how to reason about events in CVL

* Addressing code reviews

* Addressing Christiane's CR

* Issue with merge resolution

* Revert "Bug fixed"

This reverts commit 33b87b9.

* Reverse incorrect change after merge

---------

Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>
Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com>
Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com>
Co-authored-by: liav-certora <liav@certora.com>
Co-authored-by: Otakar <Otakar@certora.com>
Merge pull request #189 from Certora/master
Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com>
* CERT 8687 Realistic example

* fix spec, sanity issue

* fix

* require invariant example

* Update README

* Update CVLByExample/Invariant/RequireInvariantArray/README.md

* Addressing Nurit's CR

---------

Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com>
Co-authored-by: Johannes Spaeth <johannes@certora.com>
* Re routing example

* Updating example

---------

Co-authored-by: Johannes Spaeth <johannes@certora.com>
* Fix some of the sanity failure

* Fixing specification to not have sanity failures

runFullPool.conf -> https://vaas-stg.certora.com/output/53900/a7ab7f221da84eb4accea1c95e936803?anonymousKey=e063b8e60bae944b4a9d0d0431999b5bd4b578ea
runBroken.con -> https://vaas-stg.certora.com/output/53900/c85b8c49fec24d32ac0de00043d7ddd6?anonymousKey=a6c585f91d010a7c13f1c6d8935143b894a0c05d

* Updates to spec

* Self-Review

---------

Co-authored-by: Johannes Spaeth <johannes@certora.com>
Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>
* add an example for internal function calls

* Update CVLByExample/InternalFunctionsFromCVL/README.md

Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com>

---------

Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com>
@yoav-el-certora yoav-el-certora merged commit aa1c73e into master Aug 11, 2025
1 of 2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

8 participants