axiom-formal

Формализация семантики выражений Axiom и модели proof gate на Lean 4.

Проверенные результаты

На Lean 4.33.0 выполнен lake build: теорема absCandidate_satisfies доказывает свойство SatisfiesAbs absCandidate для всех математических целых. Теорема modifiedProgramRejected доказывает отказ политики при несовпадении идентификатора программы с receipt. Сборка не содержит sorry.

Это доказательство определения Lean. Оно не доказывает соответствие реализаций VM на Rust/Python этой семантике, криптографическую стойкость идентификаторов или безопасность исполняющей среды. Эти связи остаются отдельными исследовательскими задачами.

Воспроизведение

Установите инструментальную цепочку из lean-toolchain и выполните:

lake build

Корневой модуль Axiom.lean включает Axiom.Semantics и Axiom.ProofGate, поэтому стандартная сборка проверяет оба результата. CI загружает официальный Lean 4.33.0 и проверяет SHA-256 архива перед запуском.

Компонент проекта Axiom; общая тема — localzet-axiom. Основной язык исследований — русский. Лицензия MIT сохранена из исходного проекта.

Исходный код · MIT