The post has been translated automatically. Original language: Russian
The formal verification itself answers the technical question of whether the specified properties are met for a specific implementation. But in a real project, this is not enough. In a week, the source code may change, in a month a new version of the contract will appear, and in a year you will need to explain exactly which proof related to the released version of the system.
This requires not only a verifier, but also the management of the entire evidence-based history of the project.
Noda Assurance links requirements, implementation versions, checks performed, and evidence obtained. However, Noda does not run the compiler, tests, or formal verifier instead of the developer. Verification is performed locally, and Assurance records its exact input data, result, and related artifacts.
The main path can be represented as follows:
Requirement
│
▼
Implementation version
+
SJV
│
▼
Local verification
│
▼
Run
│
▼
SJP
│
▼
Evidence
│
▼
Confirmation
│
▼
Seal
│
▼
BaselineEach stage answers a separate question. Together, they allow us not just to say "we have tested this system," but to restore the exact chain of proof.
Assurance is not a verifier
This is the first difference that is important to understand.
Suppose a developer executes a formal verification command on his workstation:
sekura-sjv ...Or runs tests:
test-suite ...Or performs a reproducible build.
All these actions take place outside of Noda.
Noda Assurance does not attempt to remotely reproduce the user's environment and does not claim to have run these commands on its own. Instead, it fixes:
what was checked
which version of the tool
with what input data
what result did you get
what files have appeared?
who confirmed the resultThis makes the line of responsibility explicit.
The local tool is responsible for the technical verification itself. Assurance is responsible for the traceability and integrity of its evidence-based history.
It all starts with a project
In Assurance, data is organized by project.
For example:
Project: Sekura JSor:
Project: Memora8The project becomes a common domain within which requirements, implementations, verifications, proofs, and control snapshots are located.
But the project itself doesn't prove anything yet. The next question is, which statements about the system generally require confirmation?
The requirement is the center of the evidence chain
Let's say there is a requirement:
After the reset, the controller should be in the IDLE state.
In Assurance, it can be framed as a requirement or Claim — a verifiable statement.
Conditional:
REQ-017
After reset:
state = IDLEIt is around such a statement that the evidence chain is built.
You can link to it later.:
implementation
SJV
Run
EvidenceAs a result, it becomes possible to answer not only the question:
What checks did we run?
but also on a much more important one:
What confirms the specific requirement?
A work task and a requirement are not the same thing.
You can store regular work tasks in Assurance.
For example:
TASK-042
Fix reset processingBut the task itself is not considered a requirement and is not involved in the evaluation of evidence coverage.
This is a useful separation.
The task answers the question:
What needs to be done?
And the requirement:
What property of the system should be fulfilled?
After completing the task, its result may change the implementation, and the new version of the implementation should confirm the corresponding requirement.
That is:
Task
│
To change the code
A new version of the implementation
│
─
Verification of the requirementThis way, development management is not mixed with evidence management.
It is necessary to determine in advance a sufficient type of confirmation
Not every requirement needs to be supported by formal proof.
Formal verification may be required for one property, tests are sufficient for another, and reproducible assembly or engineering review is important for a third.
Assurance has a coverage policy for this.
For example, a project may require:
FORMALor:
TESTED
+
REPRODUCIBLEThe first option requires a formal certificate. In the second case, the claim is considered covered only if there is both a test and reproducible confirmation.
There are four main profiles:
FORMAL
TESTED
REPRODUCIBLE
REVIEWEDSJV and SJP refer specifically to FORMAL. The rest of the profiles have their own input data and artifacts and should not be presented as formal proof.
For formal verification, you need to fix the implementation.
The most common problem with verification reports is the loss of communication with the exact state of the source code.
Phrase:
We have checked the controller.
too vague.
You need to know:
controller
revision 17or another exact content identifier.
Therefore, in Assurance, the implementation is registered as a separate object with a specific revision.
The meaning is simple:
Implementation
controller
revision: 17If the code has changed, another revision appears.
The old proof remains in history, but it should not automatically be considered proof of a new implementation.
The same applies to SJV
The formal specification is also changing.
Suppose, initially, SJV required:
state' != ERRORLater, the contract became stricter:
state' != ERROR
counter' <= LIMITThis is another evidentiary statement.
Therefore, Assurance records separately:
Implementation revision
SJV revisionAnd the formal verification refers specifically to their specific combination.
It turns out:
Implementation rev. 17
+
SJV rev. 5
. VerificationIf either of the two inputs changes, the old result cannot be silently transferred to the new combination.
Run records the fact of the completed check
The next object is Run, that is, the specific run of the check.
Before the local launch, the input data and information about the verification tool are recorded in Assurance.
For example:
Run
────────────────────
Implementation: rev. 17
SJV: rev. 5
Checker:
sekura-sjv
Version:
2.x
Profile:
FORMALAfter that, the developer performs the verification locally.
Noda does not run the command at this point. She is waiting for the actual result of the local operation.
If the check is indeed successful, the Run can be completed with the result of a PASS.
If an error has occurred, a timeout has occurred, or the proof has failed, the actual result must be recorded.
You can't set a PASS just because such a result was expected.
Why separate Run from Evidence
At first glance, it seems that a successful Run is already enough.
But Run means:
Such a check was registered as having been performed with such inputs and such a result.
Evidence answers another question.:
What data do we accept as evidence of the fulfillment of a specific requirement?
These entities are related, but not equal.
For example:
Requirement
│
▼
Run
│
▼
SJP
│
▼
EvidenceThe same project can contain many types: successful, unsuccessful, experimental, outdated.
Evidence highlights the result that is used as the evidentiary basis for the claim.
For FORMAL, you need a real SJP
The successful Run status is not sufficient for a formal profile.
The SJP received during verification is needed.
Simplified:
Implementation
+
SJV
, ─ local verifier
│
▼
SJPThis file is uploaded to Assurance as an artifact.
Noda checks the saved bytes of the artifact and the information associated with the download. Therefore, Evidence refers not just to the name of the controller.sjp file, but to a specific uploaded object.
This is important because it is easy to leave the file name the same after changing the content.
Evidence combines evidence-based data
After the Run is completed and the necessary artifacts are loaded, Evidence is created.
For a formal profile, it can be represented as:
Evidence
│
├─ Requirement
│
├─ FORMAL
│
├─ Run
│
├─ Implementation revision
│
├─ SJV revision
└─ SJPEvidence is no longer just a file. This is an evidentiary record linking a requirement to a specific verification run and specific inputs.
It is such a record that can later be checked for relevance, confirmed and sealed.
The evidence must be related to the requirement
Let's say there are ten SJPS in the project.
Their very presence does not answer the question of what requirements they confirm.
Therefore, an explicit connection is being built.:
REQ-017
│
│ evidence_for
▼
Evidence-31This is how the traceability graph gradually appears.
It is possible to move from requirement to proof:
requirement
↓
Evidenceor examine the proof and understand what kind of statement it was created for.
This is much more useful than a folder filled with reports and files with an obscure history.
Evidence is first confirmed
Evidence may require confirmations from authorized participants before final sealing.
The account settings determine which keys or sessions can act as validators and how many confirmations are needed.
For example:
Is required:
2 confirmations
Validators:
A
B
CThen the two authorized participants must independently confirm the specific version of the Evidence.
If the Evidence changes after that, the old confirmations of the new version are not automatically transferred.
This is an important property: you cannot confirm one set of evidence and then quietly replace it with other content.
What does confirmation mean?
Confirmation in Assurance should not be interpreted too broadly.
It means that the authorized participant has confirmed a specific version of the Evidence.
This does not necessarily mean:
the man personally observed
the entire assembly process
or
Noda itself repeated
the formal verificationAssurance records the technical fact of confirmation by a certain authorized participant.
If an organization needs a more rigorous procedure, it should define it in its own work rules.
After confirmation, the Evidence can be sealed.
The next stage is the seal, or sealing of Evidence.
Before doing this, Assurance checks the necessary conditions: profile, successful Run, required artifacts, connections, confirmations, and data integrity.
For a formal profile, the chain is something like this:
Requirement
│
▼
Implementation revision
+
SJV revision
│
▼
Run = PASS
│
▼
finalized SJP
│
▼
Evidence
│
▼
required confirmations
│
▼
SEALAfter successful sealing, Evidence becomes immutable.
This is a very important boundary.
The proof record can still be prepared before the seal. After the seal, it becomes a fixed historical fact of the project.
If it is necessary to prove an already modified implementation, a new Evidence is created, rather than rewriting the old one.
Why immutability is important
Let's present the proof created for the 1.0 release.
Two months later, version 1.1 was released.
If you simply replace the reference to the new implementation inside the old record, the historical information will be lost. It will no longer be possible to establish what exactly has been proven for version 1.0.
With immutable Evidence, the history is preserved.:
Release 1.0
│
└── Evidence A
SEALED
Release 1.1
│
└── Evidence B
SEALEDThis model is especially useful for long-term engineering projects, auditing, and investigating changes.
The old proof may become irrelevant
The sealed Evidence remains unchanged, but this does not mean that it remains forever relevant to the current state of the project.
Suppose:
Evidence A
Implementation rev. 17After that, the current implementation became:
Implementation rev. 18Evidence A does not disappear or become "incorrect". It still shows the proof for rev. 17.
But regarding the current project, it is already outdated.
Assurance distinguishes between such states through freshness — the relevance of the proof.
Simplified:
The CURRENT
inputs are the same as the current ones
STALE
one or more inputs have changed
UNKNOWN
not enough data to compareThis separates historical accuracy from current applicability.
Changing SJV also makes the old Evidence irrelevant.
It's not just about the code.
Let's say the implementation hasn't changed, but a new contract has appeared.:
SJV rev. 5
↓
SJV rev. 6The new version may require additional properties to be proved.
The old SJP does not become false. He was just proving the previous contract.
A new check is required for the new SJV:
Implementation rev. 17
+
SJV rev. 6
│
─
new Run
New SJP
│
▼
new EvidenceThus, Assurance allows you to see exactly where the proof has stopped matching the current configuration.
Gap shows what is missing
For each verified requirement, Assurance can determine whether the established coverage policy is satisfied.
For example:
REQ-017
policy: FORMALIf there is no successful Run for it, there will be a gap in the proof chain.
After running, the situation may change, but if SJP is not loaded yet, another gap will remain.
Conditional:
Requirement
│
There is no Run
▼
GAPthen:
Requirement
│
▼
Run PASS
│
There is no SJP
│
▼
GAPand only after completing the entire necessary chain:
Requirement
│
▼
valid sealed Evidence
│
▼
COVEREDSo Assurance shows not just a red or green status, but allows you to understand which link is missing.
The control snapshot captures the status of the project
When the required set of requirements is covered by evidence, you can create a baseline control snapshot.
It records a certain state of the project's evidence base.
For example:
Baseline 1.0
────────────
REQ-001 → Evidence A
REQ-002 → Evidence B
REQ-003 → Evidence C
...Once created, the baseline should not change with the current project.
Development continues, new versions of requirements and evidence appear, but the old snapshot remains.
This allows you to answer the question:
What was the evidentiary status of the project at the time of the release of version 1.0?
Baseline is useful for releases
Let's imagine a typical development cycle:
development
│
Verification process
│
▼
Evidence
│
Elimination of gaps
│
▼
Baseline 1.0
│
─
Releaseclass="paragraph"> Then the work continues:
new development
│
New revisions
│
The new Evidence
▼
Baseline 1.1Now the two versions can be compared not only by source code, but also by evidence base.
You can see which requirements have changed, which evidence has become new, and which parts of the system require re-verification.
Assurance stores more than just FORMAL
Although formal verification shows the Assurance model well, the same general approach works with other profiles.
For TESTED, instead of SJP, the key supporting artifact will be the test report.
For REPRODUCIBLE, the original version, the toolkit, and the results of repeated builds are recorded.
A record of the engineering review and its scope is saved for REVIEWED.
The general scheme remains similar:
Requirement
│
A certain type of verification
│
▼
Run / supporting artifacts
│
▼
Evidence
│
▼
SealThis allows you not to pretend in one project that absolutely everything has a formal proof.
You can use a suitable confirmation level for each requirement.
What does Assurance provide in addition to file folders
You can store SJV, SJP, and reports simply in the project directory.
But then after a while there are questions:
Which SJP applies to which requirement?
Which version of the code was checked?
Which version of SJV was used?
Which file is relevant?
Who confirmed the result?
What was included in the release?
What requirements are not covered yet?The file itself does not answer these questions.
Assurance stores relationships between objects:
Requirement
│
├── implemented_by ─► Implementation
│
├── specified_by ───► SJV
│
├── verified_by ─────► Run
│
└── evidence_for ────► EvidenceIt is this graph that turns a set of individual documents into an evidence-based project history.
An example of a complete formal chain
Consider the requirement:
The controller should never enter a forbidden state.
In Assurance, the workflow may look like this:
REQ-042
"The forbidden state
is unreachable."
Implementation
controller rev. 17
│
+
SJV
controller.safety rev. 4
│
▼
Run
sekura-sjv
PASS
│
▼
controller.sjp
│
▼
Evidence
FORMAL
│
▼
confirmation
│
▼
SEALED
│
▼
Baseline 1.0Now the statement "for version 1.0, the controller satisfied REQ-042" has a specific technical chain.
If the controller rev appears later. 18, the old result will remain, but its relevance for the current version will change.
What to do after changing the code
After changing the implementation, the correct process is not to edit the old Evidence.
You need to go through a new chain:
new revision
, ─
checking for relevance
│
▼
STALE of the old Evidence
, ─
new Run
New SJP
New Evidence
, the new seal
This is not how history is destroyed.
You can see it at the same time:
what has been proven before
What has changed
what is proven nowFor an engineering project, this is much more valuable than one constantly overwritten "everything checked" status.
Assurance does not make the proof stronger than it is
It is important to understand the boundaries of the system.
If the local verifier has proven only one property, Assurance does not turn this into proof of the entire product.
If Run was mistakenly marked as successful by a human, Noda cannot magically restore the reality of the command execution.
If the confirming participant has not carried out the verification provided by the organization, the mere presence of his confirmation does not correct the process.
Assurance makes the proof chain explicit, traceable, and protected from imperceptible change. But the quality of the initial requirements, procedures, and tools remains the responsibility of the project.
The main idea
It is useful to think of Noda Assurance not as another verification tool, but as an evidence accounting system.
The formal verifier responds:
Does this property hold?
Assurance adds the following questions:
For what requirement?
For which version of the implementation?
With which version of the specification?
What check was performed?
What kind of artifact was obtained?
Who confirmed the Evidence?
Is it sealed?
Is it relevant now?
Which baseline is it included in?It is these questions that become critical when a project ceases to be a one-time experiment and begins to live for years.
As a result, the formal proof turns from a local result of the team into a part of a guided engineering story.:
requirement
│
- Accurate implementation
│
─
Verification
│
This is the proof
│
─
Confirmation
│
An immutable record
A control snapshot of the projectSo Sekura Noda Assurance allows you to know not just what was once tested, but what exactly has been proven, for which version of the system and what data confirms this.
Формальная проверка сама по себе отвечает на технический вопрос: выполняются ли заданные свойства для конкретной реализации. Но в реальном проекте этого недостаточно. Через неделю исходный код может измениться, через месяц появится новая версия контракта, а через год потребуется объяснить, какое именно доказательство относилось к выпущенной версии системы.
Для этого нужен не только верификатор, но и управление всей доказательной историей проекта.
Noda Assurance связывает требования, версии реализации, выполненные проверки и полученные доказательства. При этом Noda не запускает компилятор, тесты или формальный верификатор вместо разработчика. Проверка выполняется локально, а Assurance фиксирует её точные входные данные, результат и связанные артефакты.
Основной путь можно представить так:
Требование
│
▼
Версия реализации
+
SJV
│
▼
Локальная проверка
│
▼
Run
│
▼
SJP
│
▼
Evidence
│
▼
Подтверждение
│
▼
Seal
│
▼
BaselineКаждый этап отвечает на отдельный вопрос. Вместе они позволяют не просто сказать «мы проверяли эту систему», а восстановить точную цепочку доказательства.
Assurance — не верификатор
Это первое различие, которое важно понять.
Предположим, разработчик выполняет команду формальной проверки на своей рабочей станции:
sekura-sjv ...Или запускает тесты:
test-suite ...Или выполняет воспроизводимую сборку.
Все эти действия происходят вне Noda.
Noda Assurance не пытается удалённо воспроизвести среду пользователя и не утверждает, что самостоятельно запускала эти команды. Вместо этого она фиксирует:
что проверяли
какой версией инструмента
с какими входными данными
какой результат получили
какие файлы появились
кто подтвердил результатЭто делает границу ответственности явной.
Локальный инструмент отвечает за саму техническую проверку. Assurance отвечает за прослеживаемость и целостность её доказательной истории.
Всё начинается с проекта
В Assurance данные организованы по проектам.
Например:
Project: Sekura JSили:
Project: Memora8Проект становится общей областью, внутри которой находятся требования, реализации, проверки, доказательства и контрольные снимки.
Но сам проект ещё ничего не доказывает. Следующий вопрос — какие утверждения о системе вообще требуют подтверждения?
Требование — центр доказательной цепочки
Допустим, есть требование:
После сброса контроллер должен находиться в состоянии IDLE.
В Assurance его можно оформить как требование или Claim — проверяемое утверждение.
Условно:
REQ-017
После reset:
state = IDLEИменно вокруг такого утверждения строится доказательная цепочка.
Позже к нему можно привязать:
реализацию
SJV
Run
EvidenceВ результате становится возможен ответ не только на вопрос:
Какие проверки мы запускали?
но и на гораздо более важный:
Чем подтверждено конкретное требование?
Рабочая задача и требование — не одно и то же
В Assurance можно хранить обычные рабочие задачи.
Например:
TASK-042
Исправить обработку resetНо задача сама по себе не считается требованием и не участвует в оценке доказательного покрытия.
Это полезное разделение.
Задача отвечает на вопрос:
Что нужно сделать?
А требование:
Какое свойство системы должно выполняться?
После завершения задачи её результат может изменить реализацию, а уже новая версия реализации должна подтвердить соответствующее требование.
То есть:
Задача
│
▼
изменение кода
│
▼
новая версия реализации
│
▼
проверка требованияТак управление разработкой не смешивается с управлением доказательствами.
Нужно заранее определить достаточный вид подтверждения
Не каждое требование обязательно подтверждать формальным доказательством.
Для одного свойства может требоваться формальная проверка, для другого достаточно тестов, а для третьего важна воспроизводимая сборка или инженерное рассмотрение.
В Assurance для этого существует политика покрытия.
Например, проект может потребовать:
FORMALили:
TESTED
+
REPRODUCIBLEПервый вариант требует формального свидетельства. Во втором случае требование считается покрытым только при наличии и тестового, и воспроизводимого подтверждения.
Есть четыре основных профиля:
FORMAL
TESTED
REPRODUCIBLE
REVIEWEDSJV и SJP относятся именно к FORMAL. Остальные профили имеют свои входные данные и артефакты и не должны выдаваться за формальное доказательство.
Для формальной проверки нужно зафиксировать реализацию
Самая распространённая проблема с отчётами о верификации — потеря связи с точным состоянием исходного кода.
Фраза:
Мы проверили controller.
слишком расплывчата.
Нужно знать:
controller
revision 17или иной точный идентификатор содержимого.
Поэтому в Assurance реализация регистрируется как отдельный объект с конкретной ревизией.
Смысл простой:
Implementation
controller
revision: 17Если код изменился, появляется уже другая ревизия.
Старое доказательство остаётся в истории, но оно не должно автоматически считаться доказательством новой реализации.
То же относится к SJV
Формальная спецификация тоже меняется.
Предположим, первоначально SJV требовал:
state' != ERRORПозже контракт стал строже:
state' != ERROR
counter' <= LIMITЭто уже другое доказательное утверждение.
Поэтому Assurance фиксирует отдельно:
Implementation revision
SJV revisionИ формальная проверка относится именно к их конкретной комбинации.
Получается:
Implementation rev. 17
+
SJV rev. 5
│
▼
проверкаЕсли изменится любой из двух входов, старый результат нельзя молча переносить на новую комбинацию.
Run фиксирует факт выполненной проверки
Следующий объект — Run, то есть конкретный запуск проверки.
Перед локальным запуском в Assurance фиксируются входные данные и сведения о проверяющем инструменте.
Например:
Run
────────────────────
Implementation: rev. 17
SJV: rev. 5
Checker:
sekura-sjv
Version:
2.x
Profile:
FORMALПосле этого разработчик выполняет проверку локально.
Noda в этот момент не запускает команду. Она ожидает фактический результат локальной операции.
Если проверка действительно успешно завершилась, Run можно завершить с результатом PASS.
Если произошла ошибка, тайм-аут или доказательство не удалось, нужно записать именно фактический результат.
Нельзя ставить PASS только потому, что такой результат ожидался.
Зачем отделять Run от Evidence
На первый взгляд кажется, что успешного Run уже достаточно.
Но Run означает:
Такая проверка была зарегистрирована как выполненная с такими входами и таким результатом.
Evidence отвечает на другой вопрос:
Какие данные мы принимаем как свидетельство выполнения конкретного требования?
Эти сущности связаны, но не равны.
Например:
Requirement
│
▼
Run
│
▼
SJP
│
▼
EvidenceОдин и тот же проект может содержать много Run: удачные, неудачные, экспериментальные, устаревшие.
Evidence выделяет тот результат, который используется как доказательное основание для требования.
Для FORMAL нужен настоящий SJP
Для формального профиля успешного статуса Run недостаточно.
Нужен полученный при проверке SJP.
Упрощённо:
Implementation
+
SJV
│
▼
локальный verifier
│
▼
SJPЭтот файл загружается в Assurance как артефакт.
Noda проверяет сохранённые байты артефакта и связанные с загрузкой сведения. Поэтому Evidence относится не просто к имени файла controller.sjp, а к конкретному загруженному объекту.
Это важно, потому что имя файла легко оставить прежним после изменения содержимого.
Evidence объединяет доказательные данные
После завершённого Run и загрузки необходимых артефактов создаётся Evidence.
Для формального профиля его можно представить так:
Evidence
│
├─ Requirement
│
├─ FORMAL
│
├─ Run
│
├─ Implementation revision
│
├─ SJV revision
└─ SJPEvidence — это уже не просто файл. Это доказательная запись, связывающая требование с конкретным запуском проверки и конкретными входами.
Именно такую запись позже можно проверять на актуальность, подтверждать и запечатывать.
Evidence должно быть связано с требованием
Допустим, в проекте находится десять SJP.
Само их наличие ещё не отвечает на вопрос, какие требования они подтверждают.
Поэтому строится явная связь:
REQ-017
│
│ evidence_for
▼
Evidence-31Так постепенно появляется граф прослеживаемости.
Можно двигаться от требования к доказательству:
требование
↓
Evidenceили исследовать доказательство и понимать, для какого утверждения оно было создано.
Это гораздо полезнее папки, заполненной отчётами и файлами с непонятной историей.
Evidence сначала подтверждается
Перед окончательным запечатыванием Evidence может требовать подтверждений авторизованных участников.
В настройках аккаунта определяется, какие ключи или сессии могут выступать валидаторами и сколько подтверждений необходимо.
Например:
Требуется:
2 подтверждения
Валидаторы:
A
B
CТогда два разрешённых участника должны независимо подтвердить конкретную версию Evidence.
Если Evidence после этого изменится, старые подтверждения новой версии автоматически не переносятся.
Это важное свойство: нельзя подтвердить один набор доказательных данных, а затем тихо заменить их другим содержимым.
Что означает подтверждение
Подтверждение в Assurance не следует интерпретировать слишком широко.
Оно означает, что авторизованный участник подтвердил конкретную версию Evidence.
Это не обязательно означает:
человек лично наблюдал
весь процесс сборки
или
Noda сама повторила
формальную проверкуAssurance фиксирует технический факт подтверждения определённым разрешённым участником.
Если организации нужна более строгая процедура, она должна определить её в собственных правилах работы.
После подтверждения Evidence можно запечатать
Следующий этап — seal, или запечатывание Evidence.
Перед этим Assurance проверяет необходимые условия: профиль, успешный Run, требуемые артефакты, связи, подтверждения и целостность данных.
Для формального профиля цепочка примерно такая:
Requirement
│
▼
Implementation revision
+
SJV revision
│
▼
Run = PASS
│
▼
finalized SJP
│
▼
Evidence
│
▼
required confirmations
│
▼
SEALПосле успешного запечатывания Evidence становится неизменяемым.
Это очень важная граница.
До seal доказательную запись ещё можно подготавливать. После seal она становится зафиксированным историческим фактом проекта.
Если необходимо доказать уже изменённую реализацию, создаётся новое Evidence, а не переписывается старое.
Почему неизменяемость важна
Представим доказательство, созданное для релиза 1.0.
Через два месяца появилась версия 1.1.
Если просто заменить внутри старой записи ссылку на новую реализацию, историческая информация будет потеряна. Уже невозможно будет установить, что именно было доказано для версии 1.0.
При неизменяемом Evidence история сохраняется:
Release 1.0
│
└── Evidence A
SEALED
Release 1.1
│
└── Evidence B
SEALEDТакая модель особенно полезна для длительных инженерных проектов, аудита и расследования изменений.
Старое доказательство может стать неактуальным
Запечатанное Evidence остаётся неизменным, но это не значит, что оно навсегда остаётся актуальным для текущего состояния проекта.
Предположим:
Evidence A
Implementation rev. 17После этого текущая реализация стала:
Implementation rev. 18Evidence A не исчезает и не становится «неправильным». Оно по-прежнему показывает доказательство для rev. 17.
Но относительно текущего проекта оно уже устарело.
Assurance различает такие состояния через freshness — актуальность доказательства.
Упрощённо:
CURRENT
входы совпадают с текущими
STALE
один или несколько входов изменились
UNKNOWN
недостаточно данных для сравненияТак историческая достоверность отделяется от текущей применимости.
Изменение SJV тоже делает старое Evidence неактуальным
Это касается не только кода.
Допустим, реализация не изменилась, но появился новый контракт:
SJV rev. 5
↓
SJV rev. 6Новая версия может требовать доказать дополнительные свойства.
Старый SJP не становится ложным. Он просто доказывал предыдущий контракт.
По отношению к новому SJV требуется новая проверка:
Implementation rev. 17
+
SJV rev. 6
│
▼
новый Run
│
▼
новый SJP
│
▼
новое EvidenceТаким образом, Assurance позволяет точно увидеть, где доказательство перестало соответствовать текущей конфигурации.
Gap показывает, чего не хватает
Для каждого проверяемого требования Assurance может определить, удовлетворена ли установленная политика покрытия.
Например:
REQ-017
policy: FORMALЕсли для него нет успешного Run, появится пробел в доказательной цепочке.
После выполнения Run ситуация может измениться, но если SJP ещё не загружен, останется другой пробел.
Условно:
Требование
│
▼
нет Run
│
▼
GAPзатем:
Требование
│
▼
Run PASS
│
▼
нет SJP
│
▼
GAPи только после завершения всей необходимой цепочки:
Requirement
│
▼
valid sealed Evidence
│
▼
COVEREDТак Assurance показывает не просто красный или зелёный статус, а позволяет понять, какого именно звена не хватает.
Контрольный снимок фиксирует состояние проекта
Когда необходимый набор требований закрыт доказательствами, можно создать baseline — контрольный снимок.
Он фиксирует определённое состояние доказательной базы проекта.
Например:
Baseline 1.0
────────────
REQ-001 → Evidence A
REQ-002 → Evidence B
REQ-003 → Evidence C
...После создания baseline не должен изменяться вместе с текущим проектом.
Разработка продолжается, появляются новые версии требований и доказательств, но старый снимок остаётся.
Это позволяет ответить на вопрос:
Каким было доказательное состояние проекта в момент выпуска версии 1.0?
Baseline полезен для релизов
Представим обычный цикл разработки:
разработка
│
▼
проверки
│
▼
Evidence
│
▼
устранение gaps
│
▼
Baseline 1.0
│
▼
релизДальше работа продолжается:
новая разработка
│
▼
новые revisions
│
▼
новое Evidence
│
▼
Baseline 1.1Теперь две версии можно сравнивать не только по исходному коду, но и по доказательной базе.
Можно увидеть, какие требования изменились, какие доказательства стали новыми и какие части системы требуют повторной проверки.
Assurance хранит не только FORMAL
Хотя формальная верификация хорошо показывает модель Assurance, тот же общий подход работает и с другими профилями.
Для TESTED вместо SJP ключевым подтверждающим артефактом будет отчёт о тестировании.
Для REPRODUCIBLE фиксируются исходная версия, инструментарий и результаты повторных сборок.
Для REVIEWED сохраняется запись инженерного рассмотрения и его область.
Общая схема остаётся похожей:
Requirement
│
▼
проверка определённого типа
│
▼
Run / supporting artifacts
│
▼
Evidence
│
▼
SealЭто позволяет в одном проекте не притворяться, что абсолютно всё имеет формальное доказательство.
Для каждого требования можно использовать подходящий уровень подтверждения.
Что Assurance даёт сверх папки с файлами
Можно хранить SJV, SJP и отчёты просто в каталоге проекта.
Но тогда через некоторое время появляются вопросы:
Какой SJP относится к какому требованию?
Какая версия кода проверялась?
Какая версия SJV использовалась?
Какой файл актуален?
Кто подтвердил результат?
Что входило в релиз?
Какие требования ещё не покрыты?Сам файл не отвечает на эти вопросы.
Assurance хранит отношения между объектами:
Requirement
│
├── implemented_by ─► Implementation
│
├── specified_by ───► SJV
│
├── verified_by ─────► Run
│
└── evidence_for ────► EvidenceИменно этот граф превращает набор отдельных документов в доказательную историю проекта.
Пример полной формальной цепочки
Рассмотрим требование:
Контроллер никогда не должен переходить в запрещённое состояние.
В Assurance рабочий процесс может выглядеть так:
REQ-042
«Запрещённое состояние недостижимо»
│
▼
Implementation
controller rev. 17
│
+
SJV
controller.safety rev. 4
│
▼
Run
sekura-sjv
PASS
│
▼
controller.sjp
│
▼
Evidence
FORMAL
│
▼
confirmation
│
▼
SEALED
│
▼
Baseline 1.0Теперь утверждение «для версии 1.0 контроллер удовлетворял REQ-042» имеет конкретную техническую цепочку.
Если позже появится controller rev. 18, старый результат сохранится, но его актуальность для текущей версии изменится.
Что делать после изменения кода
После изменения реализации правильный процесс не состоит в редактировании старого Evidence.
Нужно пройти новую цепочку:
новая revision
│
▼
проверка актуальности
│
▼
STALE старого Evidence
│
▼
новый Run
│
▼
новый SJP
│
▼
новое Evidence
│
▼
новый sealТак история не разрушается.
Можно видеть одновременно:
что было доказано раньше
что изменилось
что доказано сейчасДля инженерного проекта это гораздо ценнее одного постоянно перезаписываемого статуса «всё проверено».
Assurance не делает доказательство сильнее, чем оно есть
Важно понимать границы системы.
Если локальный верификатор доказал только одно свойство, Assurance не превращает это в доказательство всего продукта.
Если Run был ошибочно отмечен как успешный человеком, Noda не может магически восстановить реальность выполнения команды.
Если подтверждающий участник не провёл предусмотренную организацией проверку, само наличие его подтверждения не исправляет процесс.
Assurance делает доказательную цепочку явной, прослеживаемой и защищённой от незаметного изменения. Но качество исходных требований, процедур и инструментов остаётся ответственностью проекта.
Главная идея
Noda Assurance полезно воспринимать не как ещё один инструмент проверки, а как систему учёта доказательств.
Формальный верификатор отвечает:
Выполняется ли это свойство?
Assurance добавляет следующие вопросы:
Для какого требования?
Для какой версии реализации?
С какой версией спецификации?
Какая проверка была выполнена?
Какой артефакт получен?
Кто подтвердил Evidence?
Запечатано ли оно?
Актуально ли оно сейчас?
В какой baseline оно вошло?Именно эти вопросы становятся критичными, когда проект перестаёт быть одноразовым экспериментом и начинает жить годами.
В результате формальное доказательство превращается из локального результата команды в часть управляемой инженерной истории:
требование
│
▼
точная реализация
│
▼
проверка
│
▼
доказательство
│
▼
подтверждение
│
▼
неизменяемая запись
│
▼
контрольный снимок проектаТак Sekura Noda Assurance позволяет знать не просто что когда-то было проверено, а что именно доказано, для какой версии системы и какими данными это подтверждается.
Share
